4 ms·

Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? In broad strokes, how does one make sure tha

Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? In broad strokes, how does one make sure that your real system indeed behaves like your model?

pron 8y ago
> Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? Absolutely, and not just critical systems. Any system that is either complex or may have some non-obvious subtleties can benefit from a specification. > In broad strokes, how does one make sure that your real system indeed behaves like your model? In general, TLA+ can be used to specify very large and very complex systems. It is currently infeasible to mechanically verify with absolute certainty that systems of such size conform to a specification, regardless of tools used. The only systems that can be verified to such an extreme extent (called end-to-end verification, namely interesting global properties are verified all the way down to the code, and even to the machine-code level) are very, very small (no more than about 10KLOC), and even then require a tremendous amount of effort by experts. Specifications should be relatively short and clear. They are therefore useful for stating your assumptions about the system, and then checking the consequences of those assumptions. Whether the assumptions are accurate, approximate or wrong can then be verified by inspection -- this is certainly feasible and commonly done in practice. There are also relatively cheap mechanical ways to check that the system conforms to the spec, but not with absolute certainty. One is called trace checking, and its possible use with TLA+ is described here: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf
- apta 8y ago
  How common is it to use TLA+ on existing/pre-built systems, to retrospectively try to find issues or bugs in them?
  - pron 8y ago
    It's hard to answer because using TLA+ in general is far from common. But among users, I would say that most cases are where they have an existing system. That was certainly how I first used TLA+ (when I realized there could be deep design issues with a system I worked on; TLA+ showed me that there indeed were two serious problems, and it also verified that my fix was correct).
  - hwayne 8y ago
    In my experience this is how a lot of people practice learning TLA+: taking systems they already know and applying TLA+ to them. The advantage of this is you already know the system pretty well and can use that to check you modeled it correctly. Also, it finds serious bugs scarily often. I've regularly received messages from people like "Yeah I tried modeling the system and it turns out we need to throw out six months of work due to a requirement bug". I wrote more about this here: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/

pron 8y ago

> Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? Absolutely, and not just critical systems. Any system that is either complex or may have some non-obvious subtleties can benefit from a specification. > In broad strokes, how does one make sure that your real system indeed behaves like your model? In general, TLA+ can be used to specify very large and very complex systems. It is currently infeasible to mechanically verify with absolute certainty that systems of such size conform to a specification, regardless of tools used. The only systems that can be verified to such an extreme extent (called end-to-end verification, namely interesting global properties are verified all the way down to the code, and even to the machine-code level) are very, very small (no more than about 10KLOC), and even then require a tremendous amount of effort by experts. Specifications should be relatively short and clear. They are therefore useful for stating your assumptions about the system, and then checking the consequences of those assumptions. Whether the assumptions are accurate, approximate or wrong can then be verified by inspection -- this is certainly feasible and commonly done in practice. There are also relatively cheap mechanical ways to check that the system conforms to the spec, but not with absolute certainty. One is called trace checking, and its possible use with TLA+ is described here: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf

apta 8y ago
How common is it to use TLA+ on existing/pre-built systems, to retrospectively try to find issues or bugs in them?
- pron 8y ago
  It's hard to answer because using TLA+ in general is far from common. But among users, I would say that most cases are where they have an existing system. That was certainly how I first used TLA+ (when I realized there could be deep design issues with a system I worked on; TLA+ showed me that there indeed were two serious problems, and it also verified that my fix was correct).
- hwayne 8y ago
  In my experience this is how a lot of people practice learning TLA+: taking systems they already know and applying TLA+ to them. The advantage of this is you already know the system pretty well and can use that to check you modeled it correctly. Also, it finds serious bugs scarily often. I've regularly received messages from people like "Yeah I tried modeling the system and it turns out we need to throw out six months of work due to a requirement bug". I wrote more about this here: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/