A major advantage of DSLs is that it is easier to apply formal verification techniques on their programs. As example, state machines can be formally analyzed in order to detect typical bugs such as: dead states, dead transitions, or non-determinism (when from a state, under certain circumstances, several transitions can be fired simultaneously). Additionally the users can define different custom checks by using an intuitive DSL. For performing analyses we use in the background the NuSMV model checker (a concise and readable introduction to model checking can be found in this book).
Our aim is to empower developers without any knowledge on mathematical logics to use formal analyses techniques. The workflow is simple and transparent to the user: once a state machine is marked as verifiable, the MPS checks wether it is written in a language subset that we can analyze. If yes, then the context menu then contains an action to run the model checker. The results of the model checker run are displayed nicely in a table:
For each of the predefined (or custom-defined) checks, the table states whether it succeeded or failed. If it failed, the table contains an example that shows how the check is violated. The table shows the example state sequence and the values of all variables. A user can click on the respective state to get it selected in the source.
The goal of integrating model checkers in mbeddr is to make model checking (almost) as easy as writing test cases. This way, we aim to convince more users of the idea that model checking (and formal verification in general) can be used in the daily work of embedded development.