Differences

This shows you the differences between two versions of the page.

Link to this comparison view

vv-lab:formal-specification-language [2015/02/18 22:12] (current)
egm created
Line 1: Line 1:
 +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 [https://​github.com/​ericmercer/​4M framework] for our modeling system of the MCAPI API is located on [http://​github.com Github]. We also have a separate framework for translating MCAPI executions traces into [https://​github.com/​ericmercer/​MP-trace-language SMT problems].
 +
 +[[MCAPI|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 ===
 +
 +* [[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 [https://​github.com/​ericmercer/​4M framework] for our modeling system of the MCAPI API is located on [http://​github.com Github]. We also have a separate framework for translating MCAPI executions traces into [https://​github.com/​ericmercer/​MP-trace-language SMT problems].
 +
 +[[MCAPI|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