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

发布时间：2021-07-09 04:42

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

【文章来源】：小型微型计算机系统. 2020,41(02)北大核心CSCD

【文章页数】：6 页

【部分图文】：

模型检查得到错误属性的反例

第1个转换说明，如果收到的数据端口绿色液压值大于等于5，则说明使用正常线路，那么令液压值等于输入的绿色液压值．第2、3、4这三个转换说明如果收到的绿色液压值green＿input小于5，则选择备用线路;收到switch事件，则系统从select＿green转变为select＿blue，即选择备用线路;当选择阀收到来自BSCU的select＿alterate值为true，即表示当前正常线路出现了问题，则使用备用线路，令选择阀的输出液压值为蓝色液压值．

它表示电源组件发生了deplted故障．图6是导致顶层事件“bscu fail twice”发生的故障树．如图所示，在这个故障树中有两个分支引起故障:一个分支是E2和E5，它们通过与门连接，一起导致事件fault＿cfg＿1的发生;另一个分支是E2和E6，也通过与门连接，导致事件fault＿cfg＿2的发生．该故障树的逻辑公式表示为:(E2∧E5)∨(E2∧E6).

【参考文献】：
期刊论文
[1]基于SAT求解器的故障树最小割集求解算法[J]. 罗炜麟,魏欧,黄鸣宇.  计算机工程与科学. 2017(04)



本文编号：3273049