摘要
该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用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.
出处
《电脑知识与技术》
2009年第10X期8448-8452,共5页
Computer Knowledge and Technology
关键词
时间自动机
实时系统
模型检查
timed automata
real-time system
model checking
