基于时间区间时序逻辑的实时系统统一模型检测

发布时间：2018-02-02 00:08

  本文关键词： 统一模型检测 实时系统 可满足性判定 时间区间时序逻辑　出处：《电子科技大学学报》2014年05期 　论文类型：期刊论文

【摘要】：在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此,该文使用一个离散时间区间时序逻辑公式建立实时系统模型,使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质,在此基础上,离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题。该文证明了新方法的有效性以及正确性,为区间实时逻辑这一类的模型检测问题提供了方法。
[Abstract]:The real time interval property of the real time interval model can not be automatically verified in the same logic framework. In this paper, a discrete time interval temporal logic formula is used to establish the real time system model. Another discrete time interval temporal logic formula is used to describe the properties of real-time systems. The unified model checking problem of discrete time interval temporal logic can be reduced to the discrete-time interval temporal logic satisfiability judgment problem which has been solved at present. This paper proves the validity and correctness of the new method. It provides a method for model checking problems such as interval real-time logic.
【作者单位】： 郑州大学信息工程学院;西安电子科技大学计算机学院;河南牧业经济学院信息工程系;
【基金】：国家自然科学基金(U1204608,U1304606,61373043) 中国博士后科学基金(2012M511588)
【分类号】：TP301;TP306
【正文快照】： Model Checking Real-Time Systems within Unified Approachof Timed Interval Temporal Logic模型检测(model checking,MC)是一种自动验证系统性质的形式化技术,得到了广泛关注、研究与使用。在实时计算模型检测领域,时间自动机(timedautomata,TA)[1]已成为建立模型的事实标

【相似文献】

相关期刊论文 前9条

1 刘瑞挺;;自动验证技术获得图灵奖[J];计算机教育;2008年23期

2 朱明,边计年,吴为民;基于CDFG和OVL的系统验证性质分类[J];计算机工程;2005年10期

3 白金山;崔楠;李祥;;行为时态逻辑TLA定理系统证明及公平性研究[J];计算机工程与设计;2010年03期

4 张轶,林惠民;带复杂数据结构的模型检测工具[J];计算机研究与发展;2004年11期

5 化志章;揭安全;薛锦云;;一种自动的形式化验证技术——模型检测[J];微计算机信息;2007年33期

6 吕正;陈昊;陈峰;吕毅;;模型检测MESIF Cache一致性协议[J];计算机工程与应用;2010年17期

7 吴立军;骆翔宇;陈清亮;;基于动态内存和状态管理的模型检测新方法[J];计算机科学;2011年11期

8 肖美华;熊昊;;模型检测中反例最小化分析[J];南昌大学学报(工科版);2008年04期

9 郭阳,李暾,李思昆;微处理器功能验证方法研究[J];计算机工程与应用;2003年05期

相关会议论文 前1条

1 李彩虹;李廉;章超;孙守卿;吴孝军;陈波;;硬件系统SystemC~(FL)模型的SPIN验证[A];2006年全国理论计算机科学学术年会论文集[C];2006年

相关重要报纸文章 前1条

1 本报记者 边歆;异常检测是阻止蠕虫攻击的最好方法？[N];网络世界;2006年

相关博士学位论文 前7条

1 林荣德;移动界程演算及模型检测应用的关键问题研究[D];华南理工大学;2010年

2 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

3 张君华;实时随机系统的分析诊断与控制研究[D];南京航空航天大学;2011年

4 高妍妍;ASIP体系结构形式化建模与验证方法研究[D];中国科学技术大学;2009年

5 万良;基于行为时序逻辑TLA的系统、规则与协议检测的研究[D];贵州大学;2009年

6 吕鸣松;实时系统最坏情况执行时间分析技术的研究[D];东北大学;2010年

7 吕正;多核处理器存储系统的验证方法研究[D];西北大学;2013年

相关硕士学位论文 前9条

1 汪永虎;基于内存和状态管理的模型检测方法[D];电子科技大学;2012年

2 安鑫;面向一类基于轮数的分布式算法的状态空间分析与模型检测[D];山东大学;2010年

3 国莹;基于共享总线的多核实时系统WCET分析[D];东北大学;2010年

4 周怀洋;多核系统上的调度策略建模与分析[D];上海交通大学;2011年

5 张鹏;Linux环境下基于MSVL的仿真与验证[D];西安电子科技大学;2013年

6 陈卫涛;动态可重构系统形式化验证工具与原型平台的设计与实现[D];东北大学;2010年

7 易良辰;普适环境下基于抽象状态机的服务组合的分析与验证[D];上海交通大学;2013年

8 李亚利;基于可能性测度的时序逻辑性质研究[D];陕西师范大学;2013年

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

，

本文编号：1483189