Integrated modular avionics system safety analysis based on model checking

2017 ◽  
Author(s):  
Hongli Wang ◽  
Tingdi Zhao ◽  
Fuchun Ren ◽  
Zeyong Jiang
Keyword(s):  
Model Checking ◽  
Safety Analysis ◽  
System Safety ◽  
Integrated Modular Avionics

scholarly journals Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games

Electronics ◽  
2019 ◽  
Vol 8 (2) ◽  
pp. 212 ◽  
Author(s):  
Xiaomin Wei ◽  
Yunwei Dong ◽  
Pengpeng Sun ◽  
Mingrui Xiao
Keyword(s):  
Model Checking ◽  
Stochastic Games ◽  
Safety Analysis ◽  
Cyber Physical Systems ◽  
System Level ◽  
Probabilistic Model Checking ◽  
Critical Systems ◽  
System Safety ◽  
Physical Systems ◽  
Analysis And Design

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.

scholarly journals Integrating Model Checking With SysML in Complex System Safety Analysis

IEEE Access ◽  
2019 ◽  
Vol 7 ◽  
pp. 16561-16571 ◽  
Author(s):  
Hongli Wang ◽  
Deming Zhong ◽  
Tingdi Zhao ◽  
Fuchun Ren
Keyword(s):  
Complex System ◽  
Model Checking ◽  
Safety Analysis ◽  
System Safety

scholarly journals Safety analysis for integrated modular avionics based on blueprints

2018 ◽  
Vol 169 ◽  
pp. 01029
Author(s):  
Jiayun Chu ◽  
Xiaohong Bao ◽  
Tingdi Zhao ◽  
Fuchun Ren
Keyword(s):  
Matrix Theory ◽  
Safety Analysis ◽  
System Management ◽  
Core Technology ◽  
Integrated Modular Avionics ◽  
Management Functions ◽  
New Generation ◽  
And Control ◽  
Relationship Of ◽  
The Mathematical Model

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.

System safety assessment based on STPA and model checking

2018 ◽  
Vol 109 ◽  
pp. 130-143 ◽  
Author(s):  
Alheri Longji Dakwat ◽  
Emilia Villani
Keyword(s):  
Model Checking ◽  
Safety Assessment ◽  
System Safety
Sign in / Sign up

Export Citation Format

Share Document