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
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Yeung, W.L.; Leung, K.R.P.H.; Wang, Ji; Dong, Wei: Modelling and model checking suspendible business processes via statechart diagrams and CSP (2007)
- Pingree, Paula J.; Mikk, Erich: The HiVy tool set (2004)