METHOD OF VERIFYING STATECHARTS BY FIXPOINT COMPUTATION

The statechart is useful for specifying real-time systems. However, th e statechart cannot be formally verified from the perspective of both states and actions. This paper proposes a verification specification l anguage, which specifies the verification property in terms of both st ates and actions, as well as timing conditions. Finally, model checkin g of the statechart, using fixpoint computation of the verification sp ecification language, is achieved. Examples verify effectiveness.