DYNAMO Project Tools

• ParaGen - ParaGen converts XMI into an intermediate representation, Para. It uses the Xerces XMI parser to analyze XMI designs. ParaGen can produce text output or be used in scripted post-processing.
• Para2Smv - Para2Smv is a tool for converting designs expressed in Para into the input format of SMV. Design models are converted by Para2SMV into SMV state machines. Guarantees expressed in CTL (Computational Tree Logic) are provided by the designer as a seperate input into Para2Smv. Para2Smv requires SmvModel to be installed.
• SmvModel - SmvModel is a collection of C++ classes that can be used to help generate SMV input files. Para2Smv uses SmvModel to translate Para files into SMV input files.
• Product Line Assembly Tool - The Product Line Assembly Tool incorporates all the Para Tools. It is currently available in binary distribution for Cygwin and Solaris only.
• Project Without A Name - OCL 1.3 parser created by Jude Nagurney (ocl_parser"at"pwan.org). It is currently being used for COGITO and the current version of DYNAMO.
• COGITO - Combination of the pwan parser from above with a Symbol Table and data file loader for use to generate mode components in DYNAMO.
• DYNAMO - Current version of the DYNAMO project that can generate some of the template files based upon a constraint passed in. Please see MS project final report for specific functionality details or read the included Manpage.
• DYNAMO2 - Current version of the DYNAMO project that can generate some of the template files based upon a constraint passed in. Please see MS project final report for specific functionality details or read the included Manpage.  This version does not use the intermediate representation.
• OpenC++ - C++ metaprogramming tool created by Shigeru Chiba, and invariant maintenance examples created with it.

Argo UML - ArgoUML is a UML design tool developed at the University of California at Irvine. Argo UML can be used to create UML specifications of mode components. Instructions for specifying and designing mode components are available in the technical documents page. The saved xmi file can be used as an input to the ParaGen program.

SMV Model Checker - SMV is a symbolic model checker originally developed at Carnegie Mellon University. It requires two sources of input: a state machine model and a guarantee to be checked. The input file for the SMV Model Checker is generated by the Para2Smv program.

Xerces XML Parser. - The ParaGen program requires the Xerxes-C parser to analyze XMI files.