3 ms·

I've personally used TLA+ for a work project, AMA. As a general rule, it's excellent for projects where you have combinatorial explosion in state: the rules fo

by ahelwer 12y ago

I've personally used TLA+ for a work project, AMA. As a general rule, it's excellent for projects where you have combinatorial explosion in state: the rules for state transitions are quite short, but number of behaviours is enormous. This is common in concurrency and distributed systems. When they're first starting out, lot of people think simple state machines are a good target for TLA+ specification, but this is not so. Generally for state machines the number of states is linear with respect to the number of rules you have, so you're better off using something like P which also generates code for you.

Jtsummers 12y ago
Years ago I spent some time trying to learn and use Z Notation (wasn't familiar with TLA+ at the time, though it existed now that I'm reading its history). My major hurdle was that this was spent on my own time as my employers weren't interested in applying formal specification tools to our work (real-time, embedded, safety critical systems, it seemed a natural fit to me, especially because the programs were actually fairly small in the scheme of things). My current employers are similarly averse to spending time on formal specifications, but we're doing embedded, real-time, wireless communication systems and again, it's a fairly natural fit (though what we develop is much larger so full post hoc analysis with this tool would be impractical, if not impossible). How difficult, in your opinion, would it be for someone with a math and CS degree (as educational background) to spin up on TLA+ in their spare time? I reasonably have 1-2 hours a night I can spend on this before I'd be eating into hobbies and social activities. I can think of several small projects that would be useful or will be started in a few weeks/months that I might be able to use as demonstrations of the utility of a system like TLA+ (requiring only an analysis of small portions of the protocol, for instance).
- ahelwer 12y ago
  It would not be very difficult to get a working understanding of TLA+. You can separate the language into two parts - specifying safety, and specifying liveness. Safety is the easy one, and with knowledge of basic predicate logic and set operations you can have a logic puzzle spec written within hours. Specifying liveness is more difficult, since it involves temporal logic and other things I didn't cover in my degree. However, Lamport says (and I've found) 95% of specs will only need boilerplate temporal logic, so don't worry about it. I taught myself through the book Specifying Systems, although Lamport now recommends the TLA+ Hyperbook. Teaching yourself TLA+ then applying it to a work project to demonstrate its value to management is a good strategy. That is the approach I took, and having a concrete project to motivate study of TLA+ is very effective.
  - Jtsummers 12y ago
    Thanks for the feedback. I'll read/work through the tutorials and Hyperbook, I've also downloaded Specifying Systems. Hopefully I have as much time as I think I do coming up. Another question, it seems they have a strong push to use the software tools (makes sense). A lot of the time that I'll have for this will be away from home, but not particularly busy (I tend to show up to places early so I often spend up to an hour at a bar/restaurant reading a book before friends arrive). In your opinion, would it be best for me to drag my laptop with me, or could I do a fair amount with paper and pencil and put it into the computer later?
    - ahelwer 12y ago
      Paper and pencil should be enough. The syntactic analyzer is nice to have but Lamport really pushes the value of writing down your thoughts in formal logic, as an act. Model checking isn't something you do iteratively - by the time you have a spec amenable to model checking, you'll pretty convinced it's correct. Mostly, model checking will catch errors where you didn't accurately translate your thoughts to TLA+.
- tjl 12y ago
  Back when I did telecommunication standards, there was a requirement for various ITU standards to contain a Z notation specification. I started to review various books on the topic and but stopped when I found out that the consensus amongst the people I dealt with was that it was very difficult and best left to a professional. I had other things to worry about, so I never spent the time to really understand it.

by ahelwer 12y ago

Jtsummers 12y ago

Years ago I spent some time trying to learn and use Z Notation (wasn't familiar with TLA+ at the time, though it existed now that I'm reading its history). My major hurdle was that this was spent on my own time as my employers weren't interested in applying formal specification tools to our work (real-time, embedded, safety critical systems, it seemed a natural fit to me, especially because the programs were actually fairly small in the scheme of things). My current employers are similarly averse to spending time on formal specifications, but we're doing embedded, real-time, wireless communication systems and again, it's a fairly natural fit (though what we develop is much larger so full post hoc analysis with this tool would be impractical, if not impossible). How difficult, in your opinion, would it be for someone with a math and CS degree (as educational background) to spin up on TLA+ in their spare time? I reasonably have 1-2 hours a night I can spend on this before I'd be eating into hobbies and social activities. I can think of several small projects that would be useful or will be started in a few weeks/months that I might be able to use as demonstrations of the utility of a system like TLA+ (requiring only an analysis of small portions of the protocol, for instance).

ahelwer 12y ago
It would not be very difficult to get a working understanding of TLA+. You can separate the language into two parts - specifying safety, and specifying liveness. Safety is the easy one, and with knowledge of basic predicate logic and set operations you can have a logic puzzle spec written within hours. Specifying liveness is more difficult, since it involves temporal logic and other things I didn't cover in my degree. However, Lamport says (and I've found) 95% of specs will only need boilerplate temporal logic, so don't worry about it. I taught myself through the book Specifying Systems, although Lamport now recommends the TLA+ Hyperbook. Teaching yourself TLA+ then applying it to a work project to demonstrate its value to management is a good strategy. That is the approach I took, and having a concrete project to motivate study of TLA+ is very effective.
- Jtsummers 12y ago
  Thanks for the feedback. I'll read/work through the tutorials and Hyperbook, I've also downloaded Specifying Systems. Hopefully I have as much time as I think I do coming up. Another question, it seems they have a strong push to use the software tools (makes sense). A lot of the time that I'll have for this will be away from home, but not particularly busy (I tend to show up to places early so I often spend up to an hour at a bar/restaurant reading a book before friends arrive). In your opinion, would it be best for me to drag my laptop with me, or could I do a fair amount with paper and pencil and put it into the computer later?
  - ahelwer 12y ago
    Paper and pencil should be enough. The syntactic analyzer is nice to have but Lamport really pushes the value of writing down your thoughts in formal logic, as an act. Model checking isn't something you do iteratively - by the time you have a spec amenable to model checking, you'll pretty convinced it's correct. Mostly, model checking will catch errors where you didn't accurately translate your thoughts to TLA+.
tjl 12y ago
Back when I did telecommunication standards, there was a requirement for various ITU standards to contain a Z notation specification. I started to review various books on the topic and but stopped when I found out that the consensus amongst the people I dealt with was that it was very difficult and best left to a professional. I had other things to worry about, so I never spent the time to really understand it.