摘要：
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 语言、时间自动机的形式规范—CT-ZIA,其能同时描述带数据约束的实时系统的时序行为性质和数据结构性质；其次,为了研究该规范上的互模拟形式化验证,给出了 CT-ZIA 上的互模拟关系定义；然后,为了互模拟算法的可判定性,对 CT-ZIA 中的时钟进行等价划分,提出了有限论域 CT-ZIA 的定义；最后,基于有限论域 CT-ZIA 模型,给出了其上互模拟检测算法,并说明其正确性。
