基于TLA的UML模型形式化验证

统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为 2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。     

带有时钟变量的线性时序逻辑与实时系统验证

为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.     

基于时序描述逻辑的UML顺序图形式化研究

在统一建模语言（UML）规范中顺序图的语义是以自然语言的形式描述的,是一种半形式化的语言,不能对系统的交互行为进行形式化分析及论证.针对UML顺序图缺乏精确的形式化描述问题,根据顺序图的时序特征,提出了增加交互操作符的UML顺序图的六元组形式化方法.对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑.应用时序描述逻辑的时态算子得到时序描述逻辑语义形式的UML顺序图.用UML顺序图描述完整的C语言执行过程,将其形式化描述,实验结果表明,这种方法是可行的.     

并发系统的操作时序逻辑描述和验证

1.引言 近年来,为了在开发一个复杂系统的过程中尽量提高系统的正确性,减少开发过中重复、较琐的工作,国内外许多学者都从逻辑的角度进行研究,用逻辑系统对并发系统程序行描述、验证,以期通过逻辑系统的简洁和严密来保证友型并发系统的正确     

密码模块的形式化设计和验证研究

该文提出了运用形式化方法对密码模块进行辅助设计和验证的研究方向。首先介绍密码模块的相关知识和研究背景,给出了如何用形式化方法验证密码模块的过程,最后讨论在验证过程中可能存在的问题及解决方案。     

工作流时序约束模型分析与验证方法

为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.     

实时系统的形式化验证

实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。     

基于时序描述逻辑的UML状态图语义

将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力,提出一种采用时序描述逻辑形式化UML状态图,对描述逻辑进行时序扩展,得到可以表示动态和时序语义的形式化规范——时序描述逻辑,给出一套UML状态图向时序描述逻辑表达式转换的规则,通过实例验证了该方法的可行性。     

基于xMAS模型的SpaceWire信誉逻辑的形式化验证

空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议, 保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。     

反应系统的连续时序逻辑表示和验证

引进一个称为LTLC的连续时间时序逻辑，用来对反应系统进行规范与验证．LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质，这样就可将系统与性质问的满足关系转化为逻辑公式间的蕴涵关系．同时，采用非负实数集作为时间域还使我们可以利用标准的存在量词来表示变量隐藏，并可用逻辑蕴涵来表示反应系统间的求精关系．该文首先给出了LTLC的一个简单介绍，然后讨论了如何使用LTLC对反应系统进行表示与推理，最后证明了一个关于LTLC的可判定性结果．此结果可用于有穷状态反应系统的自动验证．     

Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic

Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a system, is explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence.     

一个命题投影时序逻辑符号模型检测器

现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection temporal logic,简称PPTL)符号模型检测工具——PLSMC(PPTL symbolic model checker)的设计与实现过程.该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.     

混合系统的形式验证技术及其在化工过程控制中的应用

针对PLC等逻辑控制器控制连续对象的可靠性问题。给出了混合系统的形式验证的方法,即用混合矩形自动机建模,通过其商迁移的可达性分析,证明了控制程序的正确性,应用实例表明该方法是可行和有效的。     

Symbolic Algorithmic Analysis of Rectangular Hybrid Systems

This paper investigates symbolic algorithmic analysis of rectangular hybrid systems.To deal with the symbolic reachability problem,a restricted constraint system called hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces.Hybrid zones are proved to be closed over symbolic reachability operations of rectangular hybrid systems.They are also applied to model-checking procedures for verifying some important classes of timed computation tree logic formulas.To ...     

Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems

We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus.     

基于直觉模糊集的不确定时序逻辑模型

针对现有时序逻辑在描述复杂不确定时间信息方面的局限性,提出了一种基于直觉模糊集的不确定时序逻辑模型。该模型分别定义了离散论域和连续论域下的不确定点时序逻辑、点-时段时序逻辑以及时段时序逻辑的判定公式;引入直觉模糊集的犹豫度参数,使得推理结果更加精确。最后通过实例对两类不确定时间信息进行描述,并对其时序逻辑关系的可能性进行度量。通过分析表明该模型是比较优越的。     

时态逻辑与程序验证

近年来,时态逻辑大量应用于程序验证,采取的途径随使用的时态逻辑的形式和方法的不同而异。本文用自动机理论研究几种时态逻辑(LTL,BTL,POTL)的模型和模型生成子,并讨论用时态逻辑进行程序验证的的重要途径。