概率实时时态认知逻辑模型检测中抽象技术的研究

概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性.

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK2.0.0.完成了MCTK与著名的符号化模型检测工具nu Xmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nu Xmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能.

开放式体系结构数控系统实时性的建模与分析

给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)。TTM/ATRTTL提供一整套方法用于对OAC系统的硬实时性和反馈特性进行建模并使用该形式化方法在系统层对OAC系统进行建模。分别给出开环OAC,系统级逻辑控制器以及任务间通信和同步机制的TTM模型,并最终给出具有调度机制的闭环OAC系统TTM模型。该模型为系统验证体系结构的基础。最后,给出系统验证体系结构并用模型验证工具STeP和CAD工具SF2STeP实现之。在系统验证过程中,首先解决STeP中遇到的若干模型验证问题,这些问题包括重写规则,验证规则,状态爆炸问题,以及时间约束限制问题。通过模型验证试验解决OAC系统运行过程中出现的死锁以及系统各模块执行时间约束检验问题。试验结果表明该方法可以有效地对OAC系统进行建模并对系统的实时特性进行验证。

离散事件系统的面向对象实时时态着色Petri网模型

提出了由记时面向对象着色 Petri网为被控对象建模 ,用实时时态逻辑进行系统期望行为规范的实时离散事件系统面向对象实时时态着色