期刊名称：International Journal of Hybrid Information Technology
印刷版ISSN：1738-9968
出版年度：2012
卷号：5
期号：2
出版社：SERSC
摘要：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
