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

发布时间：2017-11-14 22:00

  本文关键词：基于带数据约束实时系统的互模拟检测方法

  更多相关文章： 实时系统 接口自动机 Z语言 时间自动机 互模拟检测

【摘要】：带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统,其广泛存在于航空航天、工业控制、国防等安全攸关系统,并发挥着至关重要的作用。针对这类系统的形式化建模与验证是确保其正确性和可靠性的重要途径。文中首先研究了组合接口自动机、Z语言、时间自动机的形式规范—CT-ZIA,其能同时描述带数据约束的实时系统的时序行为性质和数据结构性质;其次,为了研究该规范上的互模拟形式化验证,给出了CT-ZIA上的互模拟关系定义;然后,为了互模拟算法的可判定性,对CT-ZIA中的时钟进行等价划分,提出了有限论域CT-ZIA的定义;最后,基于有限论域CT-ZIA模型,给出了其上互模拟检测算法,并说明其正确性。
【作者单位】： 南京航空航天大学计算机科学与技术学院;
【基金】：航空科学基金(20128052064) 中央高校基本科研业务费专项资金(NZ2013306) 国家“973”重点基础研究发展计划项目(2014CB744903)
【分类号】：TP306;TP301
【正文快照】： 0引言带数据约束的实时系统[1]是指一种既带有时间约束,又带有数据变量约束的计算系统。飞行控制、核反应堆控制以及铁路调度控制等计算机控制系统都属于带数据约束的实时系统。这些系统中许多动作的完成都与时间相关,即要满足一定的时间限制,如某个动作要在一秒钟内完成;同时

【相似文献】

中国期刊全文数据库 前2条

1 钮俊;曾国荪;王伟;;绿色评价模型的互模拟等价及逻辑保持[J];计算机学报;2013年05期

2 ;[J];;年期

中国硕士学位论文全文数据库 前1条

1 邓辉;基于可能性测度的计算树逻辑与可能性互模拟[D];陕西师范大学;2013年

，

本文编号：1187145