New Approach to Verify Statechart Models
Lina Chen, Jianmin Zhao · 2011
The traditional temporal logic based Statechart model checking faces three challenges:global state space search,multipass search and writing correct temporal properties.To attack these problems,a new approach to verify Statechart models was introduced in this paper.The core of this approach is a strengthened property specification language-Property Statechart.Using property statechart,the runs of Statechart models and their consisting status were defined clearly and detailedly.Before verification,property statecharts were reconstructed into one big property tree based on the before-and-after and concurrent relationships among them.This property tree covers all the properties of target Statechart models needed to verify.In the process of verification,the state space of Statechart models is unfolded step by step.To verify a part of properties we only need to search part of state space instead of the whole state space and make sure that the statuses included by this part of state space meet the propositions specified in the corresponding nodes in the property tree.So the verification can be more efficient.Then we discussed how to verify deterministic reactive systems and non-deterministic reactive systems using our ideas.A case study illustrates the approach presented in this paper.