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?
Overview
The document provides an overview of the HiVy Toolset, a software suite developed by NASA's Jet Propulsion Laboratory (JPL) for the verification of statechart models through model checking. HiVy is designed to automate the translation of statecharts created using MathWorks Stateflow® into Promela, the input language for the SPIN model checker. This process allows for the verification of distributed software systems, helping to identify and trace logical errors.
The HiVy toolbox can operate directly on Stateflow models or utilize an intermediate format known as hierarchical sequential automata (HSA). The toolset includes several programs: SfParse and sf2hsa for parsing and converting Stateflow model files into HSA format, and hsa2pr for translating HSA into Promela. Successful parsing results in an abstract syntax tree saved in a file with the .hsa extension. If multiple model files are involved, they can be merged into a single HSA file before translation, ensuring that the scope and naming conventions of Stateflow are preserved.
The HiVy compiler generates several output files, including a Promela model of the original statechart, a file listing propositions for each state and event, and a list of proposition names for automatic property generation. These propositions are essential for formalizing linear temporal logic (LTL) properties, which are used during the verification process with SPIN.
The document emphasizes the importance of preserving the semantics of Stateflow in the generated Promela model, ensuring that the translated model accurately reflects the original design. This capability is crucial for maintaining the integrity of the verification process.
The HiVy Toolset was developed by Paula Pingree of Caltech/JPL and Erich Mikk, an independent consultant, and is available for commercial licensing. The document also includes a disclaimer regarding the use of specific commercial products and the lack of endorsement by the U.S. government or JPL.
In summary, the HiVy Toolset represents a significant advancement in the field of software verification, providing a robust framework for translating and verifying statechart models, thereby enhancing the reliability of distributed software systems.
