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

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

基于事件图的离散事件仿真模型并行检验方法

非形式化仿真模型验证方法易受主观因素的影响且具有不完备性,而传统的形式化模型检验方法由于受到状态空间爆炸问题的影响,很难处理大规模的仿真模型.并行模型检验方法以其完备性、高效性已经在工业界中得到了成功的应用,但是由于涉及到形式化规约、逻辑学以及并行计算等多项技术,应用难度较大.针对上述问题,提出了基于事件图的离散事件仿真模型并行检验方法.该方法首先对事件图在模型同步方面进行了扩展,给出了扩展事件图的形式化定义、语法及语义;然后将扩展事件图模型转换到分布并行验证环境的DVE模型,成功地将并行模型检验方法应用于仿真模型验证领域.该方法使得仿真人员无须学习新的形式化验证语言就能采用并行模型检验方法对仿真模型进行形式化验证,可降低模型并行验证的难度,从而有效提高模型验证的效率和完备性.实验结果表明了该方法的有效性,有利于扩展并行模型检验方法在仿真领域中的应用.     

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

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

基于TLA的NS安全协议分析及检测

行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑,在描述并发转移系统中,行为时序逻辑通过引入行动和行为的概念,使得系统和属性可用同一种行为时序逻辑来表示。本文首先介绍行为时序逻辑的语法、语义及简单推理规则;然后以典型的NS公开密钥协议为例,对其进行形式化分析,建立了入侵者参加的简化模型。通过对模型进行FSM建模,转化为TLA+描述的规约系统,然后对其进行TLC检测,发现其存在中间人的重放攻击。     

基于系统理论过程分析的软件安全性需求分析与验证方法

针对传统系统理论过程分析（STPA）方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题,提出一种基于STPA的软件安全性需求分析与验证方法。首先,提取软件安全性需求,并利用算法将其转化为形式化表达式;其次,建立状态图模型来描述软件安全控制行为逻辑,并将其转化为程序可读的形式化语言;最后,采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性,结果表明,该方法能够实现安全需求分析的自动化生成与形式化验证,解决了传统方法对于人工干预的依赖问题及自然语言描述问题。     

基于行为时序逻辑TLA的算法分析与验证

行为时序逻辑TLA是由Leslie Lamport提出的新的逻辑,它结合了行为逻辑和时序逻辑的特点,增强了表达能力。Dekker互斥算法最早是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。本文以PlusCal语言和TLA+预言描述了Dekker算法,并利用ToolBox模型检测工具对DEKKER并发算法进行了验证。证明该算法满足互斥属性和非饥饿属性。     

基于系统理论过程分析的软件安全性需求分析与验证方法

针对传统系统理论过程分析（STPA）方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题，提出一种基于STPA的软件安全性需求分析与验证方法。首先，提取软件安全性需求，并利用算法将其转化为形式化表达式；其次，建立状态图模型来描述软件安全控制行为逻辑，并将其转化为程序可读的形式化语言；最后，采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性，结果表明，该方法能够实现安全需求分析的自动化生成与形式化验证，解决了传统方法对于人工干预的依赖问题及自然语言描述问题。     

并发系统中谓词行为图的行为时序逻辑表达

行为时序逻辑(TLA)组合时序逻辑与行为逻辑, 可以对并发系统进行描述与验证, 它引入动作和行为的概念, 使得系统和属性可用它的规约公式表示, 但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图, 对于并发转移可以用谓词行为图进行图形化表示, 谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则, 用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性, 并用系统规约的TLA公式对谓词行为图表达能力进行证明, 表明两者具有等价性, 为描述和分析并发转换系统提供了一种可行的方法。     

基于TLA＋的BRP协议规约及验证

BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序规约语言TLA＋对BRP协议进行规约和验证的过程。首先通过自然语言非形式化地描述BRP协议的基本原理和需求，在此基础上建立了BRP的形式化模型，利用TLA＋先对不考虑实时要求的BRP进行规约，然后添加实时约束获得BRP完整的规约，最后使用模型检验器TLC验证BRP协议的各种性质。     

一种基于描述逻辑的UML模型验证方法

针对UML模型中可能会存在的概念不一致、概念冗余等语义一致性问题,该文提出一种基于描述逻辑的UML模型形式化与模型验证方法。该方法首先采用描述逻辑的子系统SHOIN（D）形式化描述UML类图、状态图以及活动图的基本模型构造,进而将UML模型转换为相应的描述逻辑本体,最终借助现有的本体推理机制验证UML模型的语义一致性问题。该方法可以为下一代的软件CASE工具实现软件模型自动推理和验证提供一种可选的技术方案。     

Improving the scalability of formal human–automation interaction verification analyses that use task-analytic models

The enhanced operator function model with communications (EOFMCs) is a task-analytic modeling formalism used for including human behavior in formal models of larger systems. This allows the contribution of human behavior to the safety of the system to be evaluated with model checking. The previous method for translating the EOFMCs into model checker input language was conceptually straightforward, but extremely statespace inefficient. This limited the applications that could be formally verified using EOFMC. In this paper, we present an alternative approach for formally representing EOFMCs that substantially decreases the model’s statespace size and verification time. This paper motivates this effort, describes how the improvement was achieved, presents benchmarks demonstrating the improvements in statespace size and verification time, discusses the implications of these results, and outlines directions for future improvement.     

Model checking response times in Networked Automation Systems using jitter bounds

Response time (RT) of Networked Automation Systems (NAS) is affected by timing imperfections induced due to the network, computing and hardware components. Guaranteeing RT in the presence of such timing imperfections is essential for building dependable NAS, and to avoid costly upgrades after deployment in industries.This investigation proposes a methodology and work-flow that combines modelling, simulation, verification, experiments, and software tools to verify the RT of the NAS during the design, rather than after deployment. The RT evaluation work-flow has three phases: model building, modelling and verification. During the model building phase component reaction times are specified and their timing performance is measured by combining experiments with simulation. During the modelling phase, component based mathematical models that capture the network architecture and inter-connection are proposed. Composition of the component models gives the NAS model required for studying the RT performance on system level. Finally, in the verification step, the NAS formal models are abstracted as UPPAAL timed automata with their timing interfaces. To model timing interfaces, the action patterns, and their timing wrapper are proposed. The formal model of high level of abstraction is used to verify the total response time of the NAS where the reactions to be verified are specified using a subset of timed computation tree logic (TCTL) in UPPAAL model checker. The proposed approach is illustrated on an industrial steam boiler deployment.     

基于梯形逻辑的联锁系统形式化验证方法

铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。     

Automated formal verification of visual modeling languages by model checking

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level.     

From verified model to executable program: the PAT approach

CSP# is a formal modeling language that emphasizes the design of communication in concurrent systems. PAT framework provides a model checking environment for the simulation and verification of CSP# models. Although the desired properties can be formally verified at the design level, it is not always straightforward to ensure the correctness of the system’s implementation conforms to the behaviors of the formal design model. To avoid human error and enhance productivity, it would be beneficial to have a tool support to automatically generate the executable programs from their corresponding formal models. In this paper, we propose such a solution for translating verified CSP# models into C# programs in the PAT framework. We encoded the CSP# operators in a C# library-“PAT.Runtime”, where the event synchronization is based on the “Monitor” class in C#. The precondition and choice layers are built on top of the CSP event synchronization to support language-specific features. We further developed a code generation tool to automatically transform CSP# models into multi-threaded C# programs. We proved that the generated C# program and original CSP# model are equivalent on the trace semantics. This equivalence guarantees that the verified properties of the CSP# models are preserved in the generated C# programs. Furthermore, based on the existing implementation of choice operator, we improved the synchronization mechanism by pruning the unnecessary communications among the choice operators. The experiment results showed that the improved mechanism notably outperforms the standard JCSP library.