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

An Approach of Bisimulation Checking for Real-time System Based on Data Constraints

作　　者：李国拯 高正[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016

出　　处：《计算机技术与发展》2016年第1期6-9,17,共5页Computer Technology and Development

基　　金：航空科学基金(20128052064);中央高校基本科研业务费专项资金(NZ2013306);国家"973"重点基础研究发展计划项目(2014CB744903)

摘　　要：带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统,其广泛存在于航空航天、工业控制、国防等安全攸关系统,并发挥着至关重要的作用。针对这类系统的形式化建模与验证是确保其正确性和可靠性的重要途径。文中首先研究了组合接口自动机、Z语言、时间自动机的形式规范—CT-ZIA,其能同时描述带数据约束的实时系统的时序行为性质和数据结构性质;其次,为了研究该规范上的互模拟形式化验证,给出了CT-ZIA上的互模拟关系定义;然后,为了互模拟算法的可判定性,对CT-ZIA中的时钟进行等价划分,提出了有限论域CT-ZIA的定义;最后,基于有限论域CT-ZIA模型,给出了其上互模拟检测算法,并说明其正确性。Real- time systems with data constraints refer to computing systems both with time- bound and data variables constraints,which is widely used in safety- critical areas like aerospace,industry control,defense system,playing an important role. Formal modeling and verification for these systems is an important way to ensure the correctness and reliability of the systems. In this paper,study a specification model combining interface automata,timed automata and Z language,named CT- ZIA. This model can be used to describe temporal properties and data properties of real- time systems with data constraints. Second,in order to study formal verification for bisimulation in the specification,the bisimulation definition for CT- ZIA is given. Then,for the decidability of simulation algorithm,each clock of CT- ZIA is partitioning in equivalence,putting forward the definition of limited domain CT- ZIA＇s. Finally,give an algorithm for checking bisimulation relation between CT- ZIAs with finite domain and demonstrate the correctness of the algorithm.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]