earticle

영어

The modeling and verification of real-time systems is a challenging task in the area of software engineering. This paper proposes a formal method for modeling and verification of real-time systems based on aspect-oriented timed statecharts and linear-time temporal logic. Behaviors of real-time systems are modeled by aspect-oriented timed statecharts, while key properties of systems are specified by linear-time temporal logic. Moreover, aspect-oriented timed statecharts are translated to timed automata with guards to simulate the executable paths of systems and model checking technologies are applied to the verification of models. An elevator example illustrates our modeling and verification method.