基于带数据约束实时系统的互模拟检测方法

• 作者: 李国拯 高正
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 实时系统 接口自动机 Z语言 时间自动机 互模拟检测
• 年，卷（期）: 2016,（1）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 6-9,17
• 页数: 5页
• 分类号: TP311
• 字数: 4880字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2016.01.002

摘要

带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统,其广泛存在于航空航天、工业控制、国防等安全攸关系统,并发挥着至关重要的作用。针对这类系统的形式化建模与验证是确保其正确性和可靠性的重要途径。文中首先研究了组合接口自动机、Z 语言、时间自动机的形式规范—CT-ZIA,其能同时描述带数据约束的实时系统的时序行为性质和数据结构性质；其次,为了研究该规范上的互模拟形式化验证,给出了 CT-ZIA 上的互模拟关系定义；然后,为了互模拟算法的可判定性,对 CT-ZIA 中的时钟进行等价划分,提出了有限论域 CT-ZIA 的定义；最后,基于有限论域 CT-ZIA 模型,给出了其上互模拟检测算法,并说明其正确性。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	高正	南京航空航天大学计算机科学与技术学院	76	907	17.0	26.0
2	李国拯	南京航空航天大学计算机科学与技术学院	2	1	1.0	1.0