Specgen is a command line tool for creating models of statecharts in the Communicating Sequential Processes (CSP) process calculus. The tool accepts an xml file in the format output by Enterprise Architect and and writes a .csp file to disk. The output is compatible with FDR3, the Oxford CSP model checker. FDR may be used to check the model for general properties, like deadlock-freedom, divergence freedom and determinism or may be compared with other CSP models using refinement.

Installation

Specgen is written in Haskell and can be built with cabal, the Haskell package manager. If you already have cabal installed, simply run cabal install from the top-level specgen directory. This should install specgen to ~/.cabal/bin. You can add this directory to your path or move the binary elsewhere.

Examples

This distribution includes many examples. See EXAMPLES.md for more information.

Usage

Usage: specgen [OPTIONS] INFILE [OUTFILE]
  -p  --printinput  Display the parsed input statechart
  -h  --help        Diplay this help message

The input file should be XML generated by Enterprise Architect. We have tested only EA 11.1. To generate the XML:

• Open a model
• From the main toolbar, select:
  Project > Model Import/Export > Export package to XMI

Credit

Specgen was primarily developed by Brandon Shapiro and Chris Casinghino.

Contact

specgen is developed by Draper Labs. Contact Chris Casinghino (ccasinghino@draper.com) for additional information.