Real-Time Systems Modeling and Verification with Aspect-Oriented Timed Statecharts
Real-Time Systems Modeling and Verification with Aspect-Oriented Timed Statecharts
复制标题
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Xinxiu Wen;Huiqun Yu
中科院分区：
文献类型：
--
作者：
Xinxiu Wen;Huiqun Yu
实时系统的建模和验证是软件工程领域的一项艰巨任务。本文提出了一种基于面向方面的时机和线性时间逻辑的实时系统建模和验证的形式方法。实时系统的行为是由面向方面的定时型statecharts建模的，而系统的关键属性则由线性时间时间逻辑指定。此外，将面向方面的定时statecharts转换为带有警卫的定时自动机，以模拟系统的可执行路径，并将模型检查技术应用于模型的验证。电梯示例说明了我们的建模和验证方法。
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.