%0 Journal Article %1 zhao_06_formal %A Zhao, Qianchuan %A Krogh, B. H. %D 2006 %J Control Systems Technology, IEEE Transactions on %K 2006 statecharts model_checking %N 5 %P 943--950 %R 10.1109/TCST.2006.876921 %T Formal verification of statecharts using finite-state model checkers %U http://dx.doi.org/10.1109/TCST.2006.876921 %V 14 %X This brief concerns the formal verification of properties of statecharts, a hierarchical state machine formalism for designing control-system logic. Various semantics have been defined for statecharts in terms of the microsteps that determine the transitions between statechart configurations. We show how computation tree logic (CTL) specifications for a statechart can be verified using a finite-state model checker such as SMV. The inputs to the model checker are a model and an associated expansion of the CTL formula that reflect the semantics. A Kripke structure with marked states provides the formal relationship between the expanded model and the original statechart structure and CTL specification. The results apply to a general class of semantics and statecharts with bounded behaviors. The approach is illustrated with a small example.

@article{zhao_06_formal, abstract = {This brief concerns the formal verification of properties of statecharts, a hierarchical state machine formalism for designing control-system logic. Various semantics have been defined for statecharts in terms of the microsteps that determine the transitions between statechart configurations. We show how computation tree logic (CTL) specifications for a statechart can be verified using a finite-state model checker such as SMV. The inputs to the model checker are a model and an associated expansion of the CTL formula that reflect the semantics. A Kripke structure with marked states provides the formal relationship between the expanded model and the original statechart structure and CTL specification. The results apply to a general class of semantics and statecharts with bounded behaviors. The approach is illustrated with a small example.}, added-at = {2009-02-11T20:59:43.000+0100}, author = {Zhao, Qianchuan and Krogh, B. H.}, biburl = {https://www.bibsonomy.org/bibtex/201bad34aad73f1e3bd630096e5acc8dd/leonardo}, citeulike-article-id = {873583}, doi = {10.1109/TCST.2006.876921}, interhash = {effcf08544e5c69b55922cc7989da847}, intrahash = {01bad34aad73f1e3bd630096e5acc8dd}, journal = {Control Systems Technology, IEEE Transactions on}, keywords = {2006 statecharts model_checking}, number = 5, pages = {943--950}, posted-at = {2006-09-26 15:18:50}, priority = {2}, timestamp = {2009-02-11T20:59:43.000+0100}, title = {Formal verification of statecharts using finite-state model checkers}, url = {http://dx.doi.org/10.1109/TCST.2006.876921}, volume = 14, year = 2006 }