We have developed a domain-specific language with an appearance resembling other modeling language such as Murphi and TCL+, that is specific to representing API state transitions and is run through a compiler to automatically output:
Ideally it would also be able to output:
FormalSpec.g – ANTLR grammar of our formal specification language
The complete framework for our modeling system of the MCAPI API is located on Github. We also have a separate framework for translating MCAPI executions traces into SMT problems.
Here is our work-in-progress on formalizing the MCAPI specification using the “Formal Spec” language.
Download the complete framework for our modeling system of the MCAPI API is located on Github. We also have a separate framework for translating MCAPI executions traces into SMT problems.