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

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

一个基于形式化方法的系统安全性建模分析实例研究

随着安全关键性系统的日益复杂,如何提高安全关键系统的安全性成为急需解决的问题.基于形式化模型的复杂系统设计与分析是一种重要的安全性分析方法.本文工作对AIR6110标准中的机轮刹车实例系统进行了基于形式化方法的安全性分析研究,包括:在系统模型设计层级对机轮刹车系统(WBS)的架构进行层次化分析,将自然语言描述的WBS系统功能用形式化语言(AADL的子集SLIM)进行严格的建模描述,消除AIR6110标准中自然语言描述存在的需求语义的二义性,从而建立了WBS系统的形式化模型;考虑系统可能发生的故障并设计多种类的故障模式,基于这些故障模式对建立的形式化功能模型进行失效行为语义的扩展,然后对获得的扩展系统模型进行安全性分析.实例分析论证了基于模型的安全性分析方法在工业系统中的有效性和实用性.     

基于UCON的网络银行在线支付及其安全性分析

通过分析现有网络银行在线支付特点及安全保护机制,发现其支付过程仍存在身份冒充、权限泄露和支付不灵活等问题。针对这些问题,提出使用控制模型UCON的网络银行在线支付模型,制定动态的授权规则和灵活的支付策略,并对提出的策略进行详细描述。通过使用模型检测工具NuSMV进行安全性分析,证明该策略符合网络银行访问控制的安全性和方便性需求,且能够弥补现有系统在身份认证机制和支付行为使用控制方面的不足。     

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

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

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

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

一种基于故障扩展SysML活动图的安全性验证框架研究

随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则;然后给出故障扩展SysML活动图的构建步骤;最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证。通过一个燃气灶控制系统验证了此方法的有效性。     

基于Django框架的故障诊断和安全评估平台

符号有向图(SDG)作为一种定性研究方法,在系统推理和图形绘制上有待改进.详细描述了计算机辅助下的SDG故障诊断和安全评估平台的开发过程.平台的开发基于开源Django框架,具有搭建维护简单、操作方便、易于二次开发等特点;利用分层SDG模型和新的推理算法实现对系统的故障诊断和安全评估,支持故障传播路径查询和分层SDG的自动绘制.以田纳西-伊斯曼过程(TEP)为例,对平台的有效性进行验证,结果证明平台推理结果完备、有效,具有实际应用的前景.     

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

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

模型驱动的软件多质量属性仿真评估方法

分析和评估复杂分布式软件系统涉及到系统功能性需求以及性能、可用性和可靠性等多种质量属性,但目前的方法一般不能同时兼顾功能性需求和非功能性需求,且往往只能针对单个质量属性进行评估。提出一种基于Discrete Event System Specification（DEVS）模型驱动的多质量属性仿真评估方法,使用扩展的Scheduled Parallel DEVS Modeling Language (SPDML)结合软件构件错误模型进行实验框架设计,实现了从图形化建模到仿真代码自动生成的全过程。     

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

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