How to use TLA+ with arKITect

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

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.