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

• 作者: 岳香芬
• 来源期刊: 电脑知识与技术
• 学科: 工学
• 关键词: 时间自动机 实时系统 模型检查
• 年，卷（期）: 2009,（30）
• 所属期刊栏目: 软件设计开发
• 页码范围: 8448-8452
• 页数: 5页
• 分类号: TP311
• 字数: 5705字
• 语种: 中文
• DOI: 10.3969/j.issn.1009-3044.2009.30.040

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	岳香芬	太原师范学院网络中心	4	6	1.0	2.0