How to use TLA+ with arKITect
It’s now possible to interface arKItect with formal proof environements. Today we talk about TLA+ interface.
There is now the possibility to configure a TLA+ export from an arKItect model. This can help validating your requirements early in the design process.
TLA+ is a high-level language for modeling programs and systems–especially concurrent and distributed ones. It’s based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors. 📌 See https://lamport.azurewebsites.net/tla/tla.html
arKItect is the most agile DSML and DSL modeler on earth. It’s low code environment.
Either with 3SE or SEA two off-the-shelf DSL for systems engineering or with a custom DSL, you can interface operational requirements descriptions with TLA+.
This approach seems very relevant when you work on System States.
In the presentation below you will find a teaser explaining the approach. Please contact us for more information.