Formal Specification Language

From Vv-lab

Revision as of 17:30, 18 November 2011 by Egm (Talk | contribs)
(diff) ← Older revision | Current revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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

Personal tools