A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and ...A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.展开更多
基金supported by the National Natural Science Foundation of China(11832012)
文摘A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.
文摘安全隐患、未遂事故等异常事件是小事故升级为重大事故的早期预警,可用来建立事故模型识别源头事件及纠正保护系统中的不安全因素。结合液化天然气(LNG)库区的工艺特点和事故特征,对系统危害辨识、预测及预防(system hazard identification,prediction and prevention,SHIPP)模型改进,提出一种将故障树、贝叶斯网络与A-star算法融合的风险评估建模方法。首先依托专家经验,结合事故报警数据库中的异常事件建立安全屏障模型和故障树;然后遵循链式法则将故障树映射为贝叶斯网络;最后与改进的A-star算法融合确定事故发生途径。基于LNG事故报警数据库的研究表明,该方法相较于传统的SHIPP模型,可以实现动态前向风险评估并量化事故之间的条件概率,反向模拟安全屏障失效时的事故发生过程。研究成果可为LNG库区的系统安全、风险规避提供合理设计及决策。
