一种基于时间自动机的实时系统模型检查算法的设计与实现

The Design and Implementation of the Model Checking Algorithm for Real-time System Based on Timed Automata

该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用Visual C++语言描述了实时特性验证中的数据结构,实现了实时特性验证算法,实验表明利用该算法可以进行实时系统的形式化验证。

This paper first gives a brief introduction of timed automata,clock region,region equivalence and clock zone. According to the region equivalence,the infinite state space of the timed automata can be transferred to the finite. Then through a typical example it describes the model checking technique for real-time system.We uses Visual C++ to implement the data structures and algorithms in the model checking of real-time properties. The correctness of these algorithms are proved by experience.