Integrated modular avionics system safety analysis based on model checking

Author(s):  
Hongli Wang ◽  
Tingdi Zhao ◽  
Fuchun Ren ◽  
Zeyong Jiang
Electronics ◽  
2019 ◽  
Vol 8 (2) ◽  
pp. 212 ◽  
Author(s):  
Xiaomin Wei ◽  
Yunwei Dong ◽  
Pengpeng Sun ◽  
Mingrui Xiao

As safety-critical systems, grid cyber-physical systems (GCPSs) are required to ensure the safety of power-related systems. However, in many cases, GCPSs may be subject to uncertain and nondeterministic environmental hazards, as well as the variable quality of devices. They can cause failures and hazards in the whole system and may jeopardize system safety. Thus, it necessitates safety analysis for system safety assurance. This paper proposes an architecture-level safety analysis approach for GCPSs applying the probabilistic model-checking of stochastic games. GCPSs are modeled using Architecture Analysis and Design Language (AADL). Random errors and failures of a GCPS and nondeterministic environment behaviors are explicitly described with AADL annexes. A GCPS AADL model including the environment can be regarded as a game. To transform AADL models to stochastic multi-player games (SMGs) models, model transformation rules are proposed and the completeness and consistency of rules are proved. Property formulae are formulated for formal verification of GCPS SMG models, so that occurrence probabilities of failed states and hazards can be obtained for system-level safety analysis. Finally, a modified IEEE 9-bus system with grid elements that are power management systems is modeled and analyzed using the proposed approach.


IEEE Access ◽  
2019 ◽  
Vol 7 ◽  
pp. 16561-16571 ◽  
Author(s):  
Hongli Wang ◽  
Deming Zhong ◽  
Tingdi Zhao ◽  
Fuchun Ren

2018 ◽  
Vol 169 ◽  
pp. 01029
Author(s):  
Jiayun Chu ◽  
Xiaohong Bao ◽  
Tingdi Zhao ◽  
Fuchun Ren

The Integrated Modular Avionics System (IMA) has been a core technology for the new generation of aircrafts in recent years. It consists of a set of reusable and interoperable common functional modules. However, the highly coupled relationship of resources makes it difficult to identify and control dangers. As an effective and efficient way, the blueprints are used to describe and manage the IMA system. Owing to the system management functions provided by the blueprints, we can accurately determine the system resources configuration status, which is very crucial for safety analysis. In this paper, we explore the possibilities to conduct safety analysis based on blueprints. A safety analysis method based on blueprints is proposed, which applies mathematical logic to describe the logical relationship between targets and resources provided by the blueprints and uses semi-tensor product of matrix theory to simplify the logical expressions. Based on the mathematical model, we can conduct the fail safety analysis and identify resources failures that may undermine the IMA system safety.


2018 ◽  
Vol 109 ◽  
pp. 130-143 ◽  
Author(s):  
Alheri Longji Dakwat ◽  
Emilia Villani

Sign in / Sign up

Export Citation Format

Share Document