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

[jarjuk <jar...@xxxxxxxxx>]

Hello,

I have made tool, which generates specification models for business IT systems in TLA+ language.
Specification model can be verified using TLA+ Tools, and parts of it can be presented as implementation blueprints to developers.

The tool address following requirements:

1. We may assume that we have an interface specification in a machine readable form. We should be able to take an interface specification, and use it to generate automatically runnable specification code.
2. Interface specifications typically define interface parameter data types without formally specifying their meaning. The solution should allow us to add meaning to interface parameters – a prerequisite before we can start defining criteria on correctness, or to model system behavior.
3. State space explosion is inherent problem in model checking, the theory behind TLA+ tool. The solution should allow us to avoid problems due to state space explosion.
4. The solution should have a code repository to store specification snippets needed to model system behavior, and correctness criteria. Assets in the code repository should be easy to include into the resulting specification code for model checking.
5. In any reasonable size business IT system, the volume of code snippets needed to model the system is going to be quite large. The solution should allow us to avoid problems caused by large specification code volume.
6. The solution should include functions for an architect to communicate implementation blueprints to a development team

Resources:

- Blog posts:

    -- https://jarjuk.wordpress.com/2016/03/03/sbuilder-1-problem/  : explains business IT context, who should benefit, and how
    -- https://jarjuk.wordpress.com/2016/03/03/sbuilder-2-intro/    : introduction to Sbuilder
    -- https://jarjuk.wordpress.com/2016/03/03/sbuilder-3-case/   : example case walk trough, process model, running the tool

- Implementation
 
   -- https://github.com/jarjuk/tla-sbuilder : code, MIT license
   -- http://jarjuk.github.io/tla-sbuilder/features.html : "live documention" (Cucumber BDD tests)


As of today (3rd March, 2016), the tool has not been yet been used to model any real world cases :(
If you have interest to the tool, you can contact me using my google mail (jarjuk) address.

BR,
Jukka


----
- Fixed date for As of today