3 ms·
So to ensure that your system follows this state machine you need to write a proof for that in some other theory (like an abstract interpretaion of your program
by jsjolen 7y ago
So to ensure that your system follows this state machine you need to write a proof for that in some other theory (like an abstract interpretaion of your program)?
- dwohnitmok 7y agoIn theory (no pun intended) yes. In practice this is not done. Perhaps never done. I know of only one toy example that you could maybe extend to do this. TLA+ is meant to double-check design level questions and intuitions rather than code level or implementation level ones. That is it attempts to give guidance on whether a design is flawed rather than whether an implementation successfully follows a specified design. This may sound limiting, but the fact that this is an artifact completely separate from code makes TLA+ much more attractive from a business risk perspective in my opinion.