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

现有模型检测工具的形式化规范语言,如计算树逻辑(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系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.     

基于SysML的复杂机电系统设计模型形式化扩展与验证

形式化系统验证是保证系统设计正确性的一种重要手段.如何针对复杂机电系统物理与软件相融合的特征,对系统设计的动态特征进行验证,是系统验证研究领域亟待解决的问题.针对这一问题,对系统工程标准建模语言SysML进行扩展,提出了一套形式化系统模型验证方法.首先,以计算树逻辑和基于流的功能表示为形式化基础,形成基于SysML的系统功能建模方法;然后,以混合自动机为基础,建立基于SysML的系统行为建模方法;最后,针对物理与软件子系统的不同动态特征,借助NuSMV模型校验器,以层次化方式实现系统模型的自动验证.以移动机器人系统为例,展示了复杂机电系统设计模型的自动验证过程.     

基于CPN的联锁进路控制建模及验证

颜色集、层次化的概念使得有色Petri网(Colored Petri Nets,CPN)能够方便地对大型复杂系统进行形式化模型验证分析,铁路车站信号计算机联锁逻辑关系形式化验证方法的研究,对于减少联锁软件开发过程中的不确定性,提高联锁系统的安全性、可靠性,保障行车安全具有重要意义,联锁系统进路控制是联锁逻辑关系的重要内容,在分析联锁进路控制的基础上,采用CPN对联锁进路控制建立形式化分析模型,为车站信号计算机联锁逻辑关系形式化验证方法的研究提供一种联锁进路控制的形式化验证方法,同时通过CPN Tools对所建立的模型进行仿真分析及状态空间分析,结果表明模型能够正确描述联锁进路控制流程及联锁进路控制的功能逻辑,且状态空间分析结果与联锁进路控制逻辑完全相符。     

WISHBONE片上总线符号模型检测

随着多核体系结构的出现和普及,片上总线逐渐成为影响片上系统功能和性能的关键部件.因此,片上总线的验证成为片上系统设计中一个重要组成部分.模型检测作为一种主流的形式化验证方法,可以自动化穷举搜索系统行为以决定片上系统的设计是否满足设计规范.然而,模型检测受制于状态空间爆炸问题,且现有规范语言如计算树逻辑和线性时序逻辑等的描述能力有限.提出了一种基于命题投影时序逻辑的WISHBONE片上总线符号模型检测方法.该方法将以Verilog硬件描述语言实现的WISHBONE总线转化为以NuSMV模型检测工具的建模语言SMV描述的系统模型,使用命题投影时序逻辑描述WISHBONE总线期望的性质,通过PLSMC工具验证系统模型是否满足期望的性质.实验结果表明该方法能够有效验证WISHBONE片上总线的定性性质,以及时间敏感和迭代性等定量性质.     

基于项重写系统的联锁系统模型检测方法研究

模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。     

基于STP方法的SCADE模型形式化验证框架

高安全性应用开发环境(SCADE)的形式化验证组件Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质,但不能充分描述拥有复杂时序性质的安全需求。为解决该问题,构建一种SCADE状态机的时序性质验证框架,将SCADE模型转换成NuSMV模型,并将线性时态逻辑和计算树逻辑引入SCADE模型的需求规范中。分析结果表明,借助NuSMV模型检查器及其验证结果可检验复杂时序相关的安全性质,减少模型设计阶段的错误,提高系统的安全性和可靠性。     

车站联锁进路控制逻辑的形式化方法

基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化 方法Event-B为基础,引入角色Agent对联锁系统进行规范定义,通过智能体与Event-B的建模和验证,构造了车站联锁进路控制逻辑形式化验证模型,并进行 了形式化规范和推理,该模型在RODIN平台上进行验证,通过实例验证,满足了计算机联锁系统的安全需求。     

CTCS-2级列控系统的形式化建模与验证

由于 CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法。分析CTCS-2级列控车载设备的模式转换场景,对其进行UML建模得到UML类图和状态图,制定转换规则对UML模型进行扩展和抽象,使其转化为NuSMV模型。将待验证的系统性质和转化后的检验程序输入符号模型检验系统进行验证,验证结果都为true,表明CTCS-2级列控车载设备的模式转化场景具有活性、可达性和安全性。     

面向需求的安全关键系统形式化建模与验证方法研究

在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML~(-e)语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML~(-e)模型转化成NuSMV 2模型的方法,并用NuSMV 2对模型的属性进行验证。针对一个真实综合航电系统中的自动飞行控制系统GFC700进行分析验证,实验结果表明,该方法对实际系统的安全性分析具有可行性。     

蒸汽锅炉安全联锁系统的形式化验证

蒸汽锅炉实时控制系统一股用于控制炉内水位,使其保持在特定的范围内。为了加强环保和生产安全,蒸汽锅炉实时控制系统等过程控制中的有关场所要设置监测报警及安全联锁系统,所以其安全联锁系统的验证也非常重要。本文采用形式化验证工具SMV(符号模型检验),根据比较安全联锁系统的输入输出是否符合安全联锁规范,检验蒸汽锅炉安全联锁系统设计的规范性。     

A Formal Verification Environment for Railway Signaling System Design

A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems.This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.     

Automated Verification of Signalling Principles in Railway Interlocking Systems

In this paper we present a verification strategy for signalling principles for the control of a railway interlocking system written in ladder logic. All translation steps have been implemented and tested on a real-world example of a railway interlocking system. The steps in this translation are as follows: 1. The development of a mathematical model of a railway interlocking system and the translation from ladder logic into this model. 2. The development of verification conditions guaranteeing the correctness of safety conditions. 3. The verification of safety conditions using a satisfiability solver. 4. The generation of safety conditions from signalling principles using a topological model of a railway yard.     

WAVer: A Model Checking-based Tool to Verify Web Application Design

Web Applications are becoming more and more widespread and efficient, then an increase of their reliability is now strongly required. Hence methods to support design and automatically perform validation of a Web Application (WA) could be helpful. In this paper we present WAVer, a prototype tool for performing the verification of a WA design by means of Symbolic Model Checking techniques. The tool first performs the modeling of the WA and furthermore verify it by means of a model checker. Specifically, the mathematical model of the WA is represented by a Finite State Machine (FSM). Then, by using the CTL formal language, we formalize basic criteria to establish correctness of the application. The prototype system we have implemented embeds a component which automatically imports WA design from a UML tool; CTL specifications are added and translated as source code for NuSMV model checker. Finally, the checker performs verification: if there is a violation of specifications, NuSMV allows to locate errors in WA design and appropriate adjustments are carried out.     

使用形式化验证方法进行流水线验证

随着流水线技术的广泛应用,流水线设计的验证问题也越来越受到业界的关注.本文提出的方法作为自上而下验证方法的一部分,可以在指令级对流水线设计的正确性进行检验.本文从控制逻辑的角度对流水线的行为进行分析,通过为控制逻辑建立FSM表示,以及采用NuSMV作为验证工具,达到对流水线的自动验证.这种方法的优势在于是以流水段为单位进行检验,这种局部验证的方法不但可以降低建模和检验的复杂度,还可以极大地缩短验证时间.     

Model checking temporal knowledge and commitments in multi-agent systems using reduction

Though modeling and verifying Multi-Agent Systems (MASs) have long been under study, there are still challenges when many different aspects need to be considered simultaneously. In fact, various frameworks have been carried out for modeling and verifying MASs with respect to knowledge and social commitments independently. However, considering them under the same framework still needs further investigation, particularly from the verification perspective. In this article, we present a new technique for model checking the logic of knowledge and commitments (CTLKC⁺). The proposed technique is fully-automatic and reduction-based in which we transform the problem of model checking CTLKC⁺ into the problem of model checking an existing logic of action called ARCTL. Concretely, we construct a set of transformation rules to formally reduce the CTLKC⁺ model into an ARCTL model and CTLKC⁺ formulae into ARCTL formulae to get benefit from the extended version of NuSMV symbolic model checker of ARCTL. Compared to a recent approach that reduces the problem of model checking CTLKC⁺ to another logic of action called GCTL¹, our technique has better scalability and efficiency. We also analyze the complexity of the proposed model checking technique. The results of this analysis reveal that the complexity of our reduction-based procedure is PSPACE-complete for local concurrent programs with respect to the size of these programs and the length of the formula being checked. From the time perspective, we prove that the complexity of the proposed approach is P-complete with regard to the size of the model and length of the formula, which makes it efficient. Finally, we implement our model checking approach on top of extended NuSMV and report verification results for the verification of the NetBill protocol, taken from business domain, against some desirable properties. The obtained results show the effectiveness of our model checking approach when the system scales up.     

A model advisor for NuSMV specifications

Among possible model validation techniques able to identify defects early in the system development, model review aims also at determining if a model is of sufficient quality, where quality is measured as the absence of certain faults. In this paper, we tackle the problem of automatic reviewing NuSMV formal specifications by developing a model advisor which helps to assure given model qualities for NuSMV programs. Vulnerabilities and defects a developer can introduce during the modeling activity using NuSMV are expressed as the violation of formal meta-properties. These meta-properties are then mapped to temporal logic formulas, and the NuSMV model checker itself is used as the engine of our model advisor to notify meta-properties violations, so revealing the absence of some quality attributes of the specification. As a proof of concept, we also report the result of applying this review process to several NuSMV specifications.     

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

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