I have made a
blog entry
documenting TLA+tools model checker performance, as a number of states
processed per second, when model checking formal models generated by
Sbuilder.
Conclusions:
- performance is CPU bound, but scalable to match real world applications
- Setups in Sbuilder can be used to manage state space explosion
-
associate Sbuilder Setups with
Use Case Slices to make the idea of
managing state space size more comprehensible for developers && implement regression verifiication
Objective:
to increase confidence in application correctness, and to make QA more
efficient with faster feed back because a formal model
- can be executed without the need to have it installed on real production environment, and
- model checker can effectively check all possible executions in a formal model.
Next:
- find a Case Study with the objective to understand applicability of creating formal models for real world applications
BR,
Jukka