[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Announcing Sbuilder - a tool to generate TLA+ model for business IT systems

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.

- 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.

- find  a Case Study with the objective to understand applicability of creating formal models for real world applications