3 ms·

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/