The HiVy toolset provides model checking for statecharts ([SFUG]). This is achieved by translating statechart specifications into the input language of the Spin model checker ([Ho197]). The HiVy toolbox transforms output of the commercial tool Stateflow@ provided by The Mathworks. HiVy can also be used independently from Stateflow. An abstract syntax of hierarchical sequential automata (HSA) is provided as an intermediate format for the toolset [Mik02]. The HiVy toolset programs include Sparse, sflhsa, hsa2pr and the HSA merge facility.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element