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.

Back

MCAPI Formalization

Here is our work-in-progress on formalizing the MCAPI specification using the “Formal Spec” language.

Thoughts on Murphi Conversion

Init/Finalize, Endpoint operations

Connectionless operations

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.

Back

vv-lab/formal-specification-language.txt · Last modified: 2015/02/18 22:12 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0