search
Table of Contents
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:
- MediaWiki-formatted documentation (using LaTex features)
- if desired: parse tree, pretty-printed (source language, minus comments) version.
Ideally it would also be able to output:
- Golden executable
- Could it generate test cases automatically?
- Keep the comments from the source to show in the documentation 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.
MCAPI Formalization
Here is our work-in-progress on formalizing the MCAPI specification using the “Formal Spec” language.
Init/Finalize, Endpoint operations
- mcapi_endpoints.fspec – fspec file
- mcapi_endpoints_doc – generated documentation
Connectionless operations
- mcapi_connectionless.fspec – fspec file
- mcapi_connectionless_doc – generated documentation
- mcapi.fspec – This is the FSpec file used in the working version of the GEM
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.
