[1]李国拯,高正. 基于带数据约束实时系统的互模拟检测方法[J].计算机技术与发展,2016,26(01):6-9.
　LI Guo-zheng,GAO Zheng. An Approach of Bisimulation Checking for Real-time System Based on Data Constraints[J].,2016,26(01):6-9.
点击复制

 基于带数据约束实时系统的互模拟检测方法()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
26
期数:
2016年01期
页码:
6-9
栏目:
智能、算法、系统工程
出版日期:
2016-01-10

文章信息/Info

Title:
 An Approach of Bisimulation Checking for Real-time System Based on Data Constraints
文章编号:
1673-629X（2016)01-0006-04
作者:
 李国拯; 高正
 南京航空航天大学 计算机科学与技术学院
Author(s):
 LI Guo-zheng; GAO Zheng
关键词:
 ; 实时系统; 接口自动机; Z语言; 时间自动机; 互模拟检测
Keywords:
 ; real-time system; interface automata ; Z notation; timed automata; bisimulation checking
分类号:
TP311
文献标志码:
A
摘要:
 带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统,其广泛存在于航空航天、工业控制、国防等安全攸关系统,并发挥着至关重要的作用。针对这类系统的形式化建模与验证是确保其正确性和可靠性的重要途径。文中首先研究了组合接口自动机、Z 语言、时间自动机的形式规范—CT-ZIA,其能同时描述带数据约束的实时系统的时序行为性质和数据结构性质；其次,为了研究该规范上的互模拟形式化验证,给出了 CT-ZIA 上的互模拟关系定义；然后,为了互模拟算法的可判定性,对 CT-ZIA 中的时钟进行等价划分,提出了有限论域 CT-ZIA 的定义；最后,基于有限论域 CT-ZIA 模型,给出了其上互模拟检测算法,并说明其正确性。
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.

相似文献/References:

[1]李行 张立臣 陈成.面向方面的实时系统中间件[J].计算机技术与发展,2008,(07):8.
　LI Xing,ZHANG Li-chen,CHEN Cheng.Aspect Oriented Middleware for Real- Time System[J].,2008,(01):8.
[2]余化鹏 卢显良 彭先蓉.基于有限的共享资源模型实现嵌入式硬实时Linux[J].计算机技术与发展,2007,(04):1.
　YU Hua-peng,LU Xian-liang,PENG Xian-rong.Implementing Embedded Hard- Real- Time Linux Based on Limited Sharing Resources Model[J].,2007,(01):1.
[3]邓惠敏 张立臣 邓建波.基于面向方面和UML的实时系统建模研究[J].计算机技术与发展,2010,(12):118.
　DENG Hui-min,ZHANG Li-chen,DENG Jian-bo.Research of Real-Time System Modeling Based on Aspect-Oriented and UML[J].,2010,(01):118.
[4]唐毓毅,朱怡安,黄姝娟,等.一种有约束关系的实时周期任务调度算法研究[J].计算机技术与发展,2013,(07):1.
　TANG Yu-yi[],ZHU Yi-an[],HUANG Shu-juan[],et al.Research on a Real-time Scheduling Algorithm for Periodic Task with Constraint Relation[J].,2013,(01):1.
[5]王宏伟,方群,陈伟.基于内存数据库的OPC监测系统的设计与实现[J].计算机技术与发展,2013,(07):242.
　WANG Hong-wei,FANG Qun,CHEN Wei.Design and Realization of OPC Real-time Monitor System Based on Main Memory Database[J].,2013,(01):242.
[6]万小平,李蜀瑜.基于XML的UML模型向AADL模型的自动转换[J].计算机技术与发展,2014,24(03):71.
　WAN Xiao-ping,LI Shu-yu.Automatic Conversion of UML Model to AADL Model Based on XML[J].,2014,24(01):71.
[7]张志宏,吴庆波,邵立松,等.基于飞腾平台TOE协议栈的设计与实现[J].计算机技术与发展,2014,24(07):1.
　ZHANG Zhi-hong,WU Qing-bo,SHAO Li-song,et al. Design and Implementation of TCP/IP Offload Engine Protocol Stack Based on FT Platform[J].,2014,24(01):1.
[8]梁文快,李毅. 改进的基因表达算法对航班优化排序问题研究[J].计算机技术与发展,2014,24(07):5.
　LIANG Wen-kuai,LI Yi. Research on Optimization of Flight Scheduling Problem Based on Improved Gene Expression Algorithm[J].,2014,24(01):5.
[9]黄静,王枫,谢志新,等. EAST文档管理系统的设计与实现[J].计算机技术与发展,2014,24(07):13.
　HUANG Jing,WANG Feng,XIE Zhi-xin,et al. Design and Implementation of EAST Document Management System[J].,2014,24(01):13.
[10]侯善江[],张代远[][][]. 基于样条权函数神经网络P2P流量识别方法[J].计算机技术与发展,2014,24(07):21.
　HOU Shan-jiang[],ZHANG Dai-yuan[][][]. P2P Traffic Identification Based on Spline Weight Function Neural Network[J].,2014,24(01):21.
[11]刘骁[],谢红梅[]. AADL行为模型时间一致性验证方法[J].计算机技术与发展,2017,27(07):1.
　LIU Xiao[],XIE Hong-mei[]. A Time Consistency Validation Approach of AADL Behavior Model[J].,2017,27(01):1.

更新日期/Last Update: 2016-04-12