时间属性序列图:语法和语义

为了表示事件出现的时间约束,扩展属性序列图为时间属性序列图,使其继承属性序列图的优点,并且能够表示时间属性,定义了时间属性序列图的形式语法,并给出基于时间Büchi自动机的形式操作语义;用实时规约模式度量了时间属性序列图的表达力。最后,对时间属性序列图进行了实例研究,显示了其广泛的应用前景。     

从活性顺序图到时态逻辑的转化方法

为了将活性顺序图用于模型检测,方便描述系统的场景需求,提出了一种将活性顺序图转换成时态逻辑的转化方法.分析活性顺序图语言并且定义一种基于路径的语义,用活性顺序图表述系统的场景需求.根据提出的语义,给出了一个将场景需求显式转化为时态逻辑的一般方法,针对并发消息较多的系统扩展和优化此方法,以得到更简短的时态逻辑公式.通过实例说明活性顺序图到线性时态逻辑的转化过程.     

多智体系统时态认知规范的模型检测算法

模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolic model verifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.     

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画.为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题.一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画.针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法.模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测.与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证.     

时态逻辑描述能力比较研究

时态逻辑在软件确认和模型检查中有广泛的应用。时态逻辑的不同变体有不同描述能力。正确理解时态逻辑的描述能力有助于书写系统特性的正确时态逻辑公式特性。论文从语法、语义域定义和语法到语义域映射三个方面对不同时态逻辑加以描述,对时态逻辑描述能力进行了比较。     

时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

行为时态逻辑TLA定理系统证明及公平性研究

行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向.为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统.在此基础上严格的证明了TIA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件.最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型.     

一种基于场景的需求验证方法

在软件需求分析工作中,需要检验获取的需求是否同客户的需求相一致.文章提出一种基于场景的软件需求验证方法,给出了基于场景的系统模型检验验证算法,并通过一个实例对其进行了检验.该方法运用有限状态自动机对软件需求进行建模,以消息序列图描述作为验证条件的场景,对获取的需求的正确性和完备性进行验证.     

基于不完全Kripke结构三值逻辑的模型检验

模型检验技术是形式化验证中比较成熟的技术，但随着设计系统规模的增加，状态爆炸已成为其发展的一个主要问题.为解决此问题，本文提出对系统进行抽象，建立不完全的状态模型，在此状态模型上来验证表示其属性的逻辑公式.这样一个逻辑公式的真值除了真、假外，还出现了第三种情况：未知，即在这个状态模型下无法确定其真值，需要更多的状态信息才能确定.本文还讨论了二值逻辑的模型检验技术，在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法，此算法与二值逻辑模型检验算法相比，没有带来时间复杂度的增加，最后给出了三值逻辑模型检验算法的应用.     

PSC2GS:一个基于属性序列图的监控器生成工具

在开放和动态环境下,系统或环境的不安全的运行时变化可能为整个系统的正确执行埋下隐患,可能最终导致软件失效。基于监控器的软件运行时验证技术已经成为开放环境下侦测软件失效行为的基本方法,该工具采用了一种基于博弈论的从Property Sequence Charts(属性序列图)中自动生成监控器的方法。监控器被赋予多值语义:满足、无限可控、系统有限可控、系统紧急可控、环境有限可控、环境紧急可控以及违例。监控器可以提供足够的信息用来预测系统失效。正文中将描述一个名为"PSC2GS"的工具,该工具具有设计属性序列图、基于属性序列图生成博弈结构、基于博弈结构生成Aspect Oriented Programming(面向方面编程)代码(监控器)等一系列功能。PSC2GS提供的完全图形化的前端接口使软件设计者可以不用处理任何特殊的文本或者逻辑公式。