HiVy is a software tool set that enables verification through model checking of designs represented as finite-state machines or statecharts. HiVy provides automated translation of (1) statecharts created by use of the MathWorks Stateflow® program to (2) Promela, the input language of the Spin model checker, which can then be used to verify, or trace logical errors in, distributed software systems. HiVy can operate directly on Stateflow models, or its abstract syntax of hierarchical sequential automata (HSA) can be used independently as an intermediate format for translation to Promela. In a typical design application, HiVy parses and reformats Stateflow model file data using the programs SfParse and sf2hsa, respectively. If the parsing effort is successful, an abstract syntax tree is delivered into a file named with the extension ".hsa." If the design comprises several model files, they may be merged into one ".hsa" file before translation into Promela. Stateflow scope is preserved, and name clashes are avoided in the merge process. The HiVy program hsa2pr translates the model from the intermediate HSA format into Promela. Additionally, HiVy provides through translation a list of all statechart model propositions that are the means for formalizing linear temporal logic (LTL) properties about the model for Spin verification.

This tool set was written by Paula Pingree of Caltech/JPL and Erich Mikk (independent consultant) for NASA's Jet Propulsion Laboratory

This software is available for commercial licensing. Please contact Don Hart of the California Institute of Technology at (818) 393-3425. Refer to NPO-30847.

This Brief includes a Technical Support Package (TSP).
Software for checking statecharts

(reference NPO30847) is currently available for download from the TSP library.

Don't have an account? Sign up here.