安全关键系统需求形式化建模分析实例研究*

近年来,基于模型的安全性分析技术(MBSA)在航空等领域有着广泛应用,因此对以xSAP安全分析平台为核心,基于MBSA的系统安全性评估方法进行了研究,并通过一个真实的综合航电系统Garmin G1000的自动飞行控制系统(AFCS)GFC700为实例来详细介绍。该方法的实现包括使用NuSMV形式化语言对系统进行需求建模,根据系统设计故障模式,在NuSMV模型中注入故障事件,使用xSAP对NuSMV需求模型进行模型扩展得到故障扩展模型,以及对故障扩展模型进行故障分析及系统安全性评估,例如生成故障树及FMEA表等。从分析结果来看,使用xSAP平台对实际系统进行基于模型的系统安全分析是行之有效的。     

基于NuSMV的AADL行为模型验证的探究

鉴于模型在软件系统开发中日趋重要的地位和AADL模型在嵌入式软件建模中的良好应用前景,为了在嵌入式软件系统开发前期保证AADL模型的质量,提出了一种基于模型测试的AADL架构和NuSMV模型的验证方法。文中首先对当前的AADL发展情况作简单介绍,然后对NuSMV验证模型的结构作大致分析,在随后的文章中对NuSMV的验证过程作详细的介绍。与此同时,使用具体的汽车巡航控制系统作为实例进行具体分析。文中通过测试用例执行输出进行验证来判断该方法的正确性。     

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

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

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

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

基于MTRDL的自动飞行系统模式需求建模与验证方法[1]

在民机自动飞行过程中,自动飞行系统模式转换是影响安全的重要因素,随着现代民机机载系统的功能与复杂度的快速增长,在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战.飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系,还体现在模式转换与外部环境之间复杂的数据与控制交联关系,这些交联关系同时隐含了飞行模式转换的安全性质,这些特征提高了形式化方法的应用难度.本文工作提出一种领域特定的建模验证框架:首先,提出面向自动飞行系统模式转换的领域需求建模语言MTRDL,和基于该语言扩展于SysML上的建模方法;其次,提出基于安全需求模板的安全性质辅助规约方法;最后,通过对某机型的若干条目化需求的实例研究,证明了本文方法在自动飞行系统模式转换需求验证中的有效性.     

一种基于模型检验程序分析技术的前端工具研究

提出了一种用模型检验技术对程序进行分析的方法,其主要思想是将C/C++源代码转换为与控制流图等价的Kripke结构,用CTL公式描述待验证的源程序性质,使用NuSMV模型检验工具实施具体的程序分析。基于这一思想,设计并实现了一个自动将C/C++源代码转换为NuSMV输入的工具。所做的实验验证表明,该方法能够有效地对程序进行分析。     

一种基于MBSE的飞行传感器系统需求建模方法

针对传统的基于文档式的需求工程方法无法满足当前复杂系统的需求分析,论文提出一种基于模型系统工程(Model-Based Systems Engineering,MBSE)思想的传感器系统需求建模分析的方法,辅以DOORS工具对需求进行管理。首先,基于DOORS对飞行传感器系统的需求管理进行研究,以支持系统的需求演进,方便后续的需求建模分析;其次,在Rhap?sody环境下采用SysML用例图对飞行传感器系统需求进行静态建模分析,从参与者的角度分析系统需求用例;最后,通过对某型号无人机传感器系统应用实例的分析来验证该方法的有效性和可行性。     

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

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

基于SPIN的HMSC模型自动检验方法

自动检测与验证HMSC (high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义，为此提出一种为HMSC模型进行自动检验的方法，并将其实现。利用转换规则为HMSC模型生成Promela检测语言，借助SPIN工具对需求进行验证。该方法不仅支持模型检测，同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具，通过一个实例展示其自动建模检测分析的效果，表明了其有效性和实用性。     

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

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

CTCS-1级列控系统等级转换场景建模与验证

随着CTCS-1级列控系统关键技术研究工作的开展,必然要面临装载CTCS-1级车载设备的列车跨线运营至CTCS-0级线路的问题,而系统等级转换的顺利进行是实现列车安全跨线运营的基础。通过系统功能分析,建立了系统多分辨率功能模型,以识别等级转换场景需求;根据场景需求,结合现行系统规范,完善了CTCS-1级系统等级转换场景的方案;采用基于UML的NuSMV建模与验证方法,建立了等级转换场景的UML模型和NuSMV模型,并验证了场景模型的活性、确定性等属性,从而证明了完善后的场景方案满足场景需求,且符合系统规范。文中对CTCS-1级系统等级转换场景的探讨可为相关规范的修订提供支持。     

Proving the shalls

Incomplete, inaccurate, ambiguous, and vola-tile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods offers developers of safety-critical systems a powerful new approach to the early validation of requirements. This paper describes an exercise conducted to determine if formal methods could be used to validate system requirements early in the lifecycle at reasonable cost. Several hundred functional and safety requirements for the mode logic of a typical flight guidance system were captured as natural language “shall” statements. A formal model of the mode logic was written in the RSML^−e language and translated into the NuSMV model checker and the PVS theorem prover using translators developed as part of the project. Each “shall” statement was manually translated into a NuSMV or PVS property and proven using these tools. Numerous errors were found in both the original requirements and the RSML^−e model. This demonstrates that formal models can be written for realistic systems and that formal analysis tools have matured to the point where they can be effectively used to find errors before implementation. This project was partially funded by the NASA Langley Research Center under contract NCC1-01001 of the Aviation Safety Program.     

信息物理融合系统的时间需求一致性分析

信息物理融合系统(cyber-physical system,简称CPS)蕴藏着巨大的潜在应用价值.时间在CPS中起到非常重要的作用,应该在需求早期阶段明确.提出了一个基于逻辑时钟的CPS时间需求一致性分析框架.首先,构建了CPS软件的时间需求概念模型,提供时间需求和功能需求的基本概念,并给出了概念模型的形式化语义;然后,在模型制导下,从CPS的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义,定义了时间需求规约的一致性特性.为了支持形式化验证,将时间需求规约转换成NuSMV模型,用CTL公式表述要检测的特性,并使用NuSMV工具实施了一致性检测.     

模拟实时系统的点区间优先级时间Petri网与TCTL验证

时间Petri网为实时系统提供了一种形式化的建模方法, 时间计算树逻辑(TCTL)为描述实时系统与时间相关的设计需求提供了一种逻辑化的表达方式, 因此基于时间Petri网的TCTL模型检测广泛应用于实时系统的正确性验证.然而对于一些涉及优先级的实时系统, 例如多核多任务实时系统, 这里不仅需要考虑任务之间的时间约束还要考虑任务执行的优先级以及引入优先级带来的抢占式调度问题, 致使相应的建模和分析变得更加困难.为此, 本文提出了点区间优先级时间Petri网, 通过在时间Petri网上定义变迁发生的优先级以及变迁的可挂起性, 从而可以模拟实时系统的抢占式调度机制, 即首先高优先级的任务抢占低优先级的任务所占用的资源, 导致后者被中断, 然后前者执行完毕后释放资源, 最后后者再次获得资源从中断的地方恢复.本文通过点区间优先级时间Petri网来模拟多核多任务实时系统, 使用TCTL来描述它们的设计需求, 设计了相应的模型检测算法, 开发了相应的模型检测器以验证它们的正确性.我们通过一个实例来说明我们的模型和方法的有效性.     

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.     

基于π演算的工作流模型检验

为保证工作流模型语义的正确性,提出一种基于π演算的工作流模型语义性质检验方法。采用π演算的一个子集πN演算描述工作流模型,证明该模型的反应关系能够终止,构造有限反应迁移图算法,利用NuSMV检验工作流模型是否满足线性时序逻辑性质。实验结果证明了该检验方法的有效性。     

包含时间约束的作战任务建模与验证方法

制定作战计划时往往需要考虑作战任务的时间约束问题。目前对作战任务的时间约束分析方法都存在约束类型少、验证方法适用范围小等问题。为此提出基于业务流的作战任务时间约束建模方法,构建了作战任务流模型并用以描述作战任务的相对和绝对时间约束。提出了作战任务的时间约束形式化验证方法,设计了作战任务模型到NuSMV语言的转换算法,并基于时序逻辑给出了作战任务的基本时间约束描述方法。最后以登岛作战任务为例,验证了其相对约束和绝对约束的部分性质,并根据反馈结果对模型进行了修正。