Table of Contents
- Background Information
- User’s Guide
- Developer’s Guide
Read an article “How Amazon uses formal methods”
Emerging API Ecosystems
blog entry argues that managing on-line openness has become more important for businesses with the emergence of API ecosystems, and, in the future, it will be even more important as blockchain technologies mature. To help in managing on-line openness this post suggests modeling API ecosystem.
A Tool To Generate Runnable Specification Models in TLA+ language
Announcing Support for Ethereum
Sbuilder Roadmap v1
Using Sbuilder to Model a Salesforce Application
Tla-sbuilder Salesforce API plugin User’s Guide
Using Sbuilder to Model Business IT Systems
post examines TLA+tools model checker performance, as a number of states processed per second, when model checking formal models generated by Sbuilder. It finds the performance to be CPU bound, but scalable to match real world applications.
The blog entry demonstrates, how Setups in Sbuilder can be used to manage state space explosion, and associates setups with Use Case Slices to make the idea of managing state space size more comprehensible for developers. Ideally, a Use Case Slice, identified in development, is configured as an Sbuidler Setup and added into a repository for Regression Verification. The objective is 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
- the model checker can effectively check all possible executions in the formal model.