J. Qian and B. Xu (PRC)
Model checking, Statecharts, LTS, process algebra
Model checking is one of the most practical techniques of automatic formal verification to ensure the correctness of design specifications. Statecharts, which extends the finite state machine, is a visual language for specifying the behavior of complex reactive system. We develop an algorithm that model check Statecharts based on labeled transition system (LTS). Firstly, term syntax and semantics of Statecharts is briefly introduced. Secondly, based on process algebra, we translate Statecharts into LTS by concurrent interleaving sequences and transition rules. Finally, a model checking algorithm to verify whether Statecharts satisfies the required properties described by computation tree logic is discussed. The results suggest that model checking Statecharts is efficient on LTS that result from Statecharts.
Important Links:
Go Back
