Model Checking Statecharts Based on EHA
Lingzhong Zhao · Jisuanji gongcheng · 2006
Model checking is one of the most practical techniques of automatic formal verification to ensure the correctness of design specifications.Statecharts that extends traditional finite state machines is a visual language for specifying the behavior of complex reactive system.The paper gives an approach of model checking Statecharts based on EHA for verifying whether Statecharts model satisfies the required properties.Firstly,it converts the system model Statecharts into the Buchi automaton ASC by EHA operation semantics,and builds the Buchi automaton A?φ.for LTL formula φ.Secondly,constructs the product automaton ASC ?A?φ.Finally,checks whether the product automaton generates the empty languages,and verifies whether Statecharts satisfies the required properties.