Modeling Adversaries with TLA+

Post by contingencies » Wed, May 08, 2019, 5:55 AM UTC

lopsidedBrain wrote: post #9

contingencies wrote: post #7

Used TLA+ for security/availability modeling at a previous venture. Didn't find it added more value than other formal methods with less scope and ambition when it came to implementation, but I had very limited resources and we were greenfield so the experience probably wasn't generally applicable. IMHO (from an implementation perspective): (1) If state is a pain to model, this may be a symptom you aren't placing inte…

> Didn't find it added more value than other formal methods with less scope and ambition For my own future reference, can you list a few other formal methods?

Post by carlmr » Wed, May 08, 2019, 7:58 AM UTC

contingencies wrote: post #11

lopsidedBrain wrote: post #9

Earlier quoted context omitted.

> Didn't find it added more value than other formal methods with less scope and ambition For my own future reference, can you list a few other formal methods?

Well, for some definition of formal, both state machines and rigorously defined {interfaces|message sequences|protocols} (ie. those with specification-based, generative implementations of endpoints, validating middleware proxies, etc.). There are two models of reality that I find to be the most useful ones, especially when writing programs. The first is functions, and the second is sequences of states. - Leslie Lampo…