计算机技术与发展Issue(1)：6-9,17,5.DOI:10.3969/j.issn.1673-629X.2016.01.002
基于带数据约束实时系统的互模拟检测方法
An Approach of Bisimulation Checking for Real-time System Based on Data Constraints
摘要
Abstract
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 specifica-tion 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语言/时间自动机/互模拟检测Key words
real-time system/interface automata/Z notation/timed automata/bisimulation checking分类
信息技术与安全科学引用本文复制引用
李国拯,高正..基于带数据约束实时系统的互模拟检测方法[J].计算机技术与发展,2016,(1):6-9,17,5.基金项目
航空科学基金(20128052064) （20128052064）
中央高校基本科研业务费专项资金( NZ2013306) （ NZ2013306）
国家“973”重点基础研究发展计划项目(2014CB744903) （2014CB744903）
