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

来源：计算机技术与发展杂志2016年第01期北京时间：

作者：李国拯;高正

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

关键词：实时系统;接口自动机;Z语言;时间自动机;互模拟检测