超协调时序逻辑及其模型检测方法

发布时间：2020-04-07 00:08

【摘要】：传统的观点认为保持系统刻画的协调性1是并发系统开发过程基本的要求,但随着所设计并发系统的规模越来越大,功能越来越复杂,使得自始至终维持系统的协调性成为一个具有挑战性的课题。分布式的开发方式,系统信息所固有的不确定性,进一步恶化了维持系统刻画协调性的难度和代价。因此我们需要一种超越经典逻辑观念的方法学,以一种合理的方式处理含有非协调信息的系统刻画 经典逻辑具有许多直觉的属性和较强的表达、推理能力,适于刻画并发系统。但由于平凡推理的缘故,含有非协调性的形式刻画无意义。基于超协调逻辑的方法学,通过把时序的观念与超协调性的方法学相结合,本文提出了一种时序逻辑QCTL(Quasi-classical temporal logic),一方面,QCTL具有刻画并发系统时序属性的能力,另一方面,避免了非协调情形下的平凡推理问题。本文主要研究QCTL逻辑体系,包括它的语义学、证明系统及基于QCTL的模型检测问题。 为了取得形式推理上的超协调性,QCTL的证明系统与经典逻辑有着显著的差别。这个证明系统是由两种不同的推理规则构成,分为分解规则和合成规则。一个具体的证明过程由分解过程和合成过程两部分组成,并且分解过程应用分解规则,合成过程应用合成规则,这样就避免了一些能导致平凡推理的证明理论。同时,我们给出了该证明系统的可靠性和完备性证明。QCTL的语义由paraKripke结构表达,它是标准Kripke结构的一种扩展。通过这种扩展,在语义层次上解开公式α和?α之间的联系,取得了语义上的超协调性,可以用于刻画、推理含有非协调信息的并发系统。 经典时序逻辑的模型检测问题得到了广泛而且深入的研究,例如CTL和LTL,但由于QCTL的逻辑理论的特殊性,传统的方法学并不适用。基于
【学位授予单位】：中国科学院研究生院（成都计算机应用研究所）
【学位级别】：博士
【学位授予年份】：2006
【分类号】：TP302

【共引文献】

相关期刊论文 前10条

1 付敏;;语义封闭性、“真矛盾论”与“悖论逻辑”[J];安徽大学学报(哲学社会科学版);2009年05期

2 刘志锋;葛云;章东;周从华;;知识时态逻辑有界模型检测中的完备性(英文)[J];Journal of Southeast University(English Edition);2010年03期

3 虞蕾;赵宗涛;;PSL的有界模型检验[J];电子学报;2009年03期

4 刘春;王越;金芝;;基于知识的软件可信性需求获取[J];电子学报;2010年S1期

5 段采宇;张维明;余滨;;武器装备需求问题框架及特性分析[J];国防科技大学学报;2009年03期

6 杜国平;;经典逻辑视野中的弗协调逻辑[J];华南师范大学学报(社会科学版);2007年05期

7 Walter Hussak;;Formal Reduction of Interfaces to Large-scale Process Control Systems[J];International Journal of Automation & Computing;2007年04期

8 ;Formal verification of safety protocol in train control system[J];Science China(Technological Sciences);2011年11期

9 ;Capability description and discovery of Internetware entity[J];Science China(Information Sciences);2010年04期

10 周从华;陈振宇;鞠时光;;基于SAT的软件验证[J];计算机研究与发展;2008年S1期

相关博士学位论文 前10条

1 杨琛;打结不变的命题投影时序逻辑与模型检测[D];西安电子科技大学;2010年

2 舒新峰;投影时序逻辑的完备公理系统与形式验证[D];西安电子科技大学;2010年

3 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

4 涂钰青;基于IEC61499标准的组件化模型集成数控系统形式化建模与验证的研究[D];华南理工大学;2011年

5 陈靖;带实时的传值与移动系统研究[D];中国科学院研究生院（软件研究所）;2003年

6 蒋建民;对称与动作细化[D];中国科学院研究生院（成都计算机应用研究所）;2006年

7 孙秀莉;基于动作细化的异步电路自动综合[D];中国科学院研究生院（成都计算机应用研究所）;2005年

8 江敏;多视点需求工程中不一致性的检测与处理[D];武汉大学;2007年

9 张海宾;混合系统的形式化验证[D];西安电子科技大学;2007年

10 邓小妮;基于模型检验与仿真的C~4ISR系统需求验证方法研究[D];国防科学技术大学;2008年

相关硕士学位论文 前10条

1 韩冰;线性时序逻辑在失业保险审计中的应用研究[D];哈尔滨工程大学;2010年

2 贺杨成;基于RCP的GIS系统及聚类技术研究[D];江南大学;2011年

3 高静;面向环境演算系统的模型检测算法的研究[D];南京航空航天大学;2009年

4 余加振;基于OOR框架的作战任务分析方法研究[D];国防科学技术大学;2010年

5 刘友澈;纺织车间集散型生产管理与监测系统研究[D];电子科技大学;2011年

6 王莉萍;基于网络的工业设计信息系统的研究与实现[D];西北工业大学;2003年

7 徐艺;人机工程设计信息系统研究[D];西北工业大学;2004年

8 徐雨波;实时系统模型检测工具FPTAT的算法与实现[D];中国科学院研究生院（软件研究所）;2005年

9 李明宇;UML模型一致性检测的研究[D];山东大学;2005年

10 王朝阳;军队院校数字化校园建设问题研究[D];国防科学技术大学;2005年

，

本文编号：2617184