swMATH ID: 1933
Software Authors: Paula J. Pingree, Erich Mikk
Description: 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.
Homepage: http://trs-new.jpl.nasa.gov/dspace/bitstream/2014/11205/1/02-3112.pdf
Programming Languages: None
Operating Systems: None
Dependencies: None
Keywords: state-charts; model checking; translation; Stateflow; Spin
Related Software: PROMELA; StateFlow; SPIN
Cited in: 2 Publications

Citations by Year