Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games
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 ha...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2019-02-01
|
| Series: | Electronics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2079-9292/8/2/212 |
| _version_ | 1811187160163811328 |
|---|---|
| author | Xiaomin Wei Yunwei Dong Pengpeng Sun Mingrui Xiao |
| author_facet | Xiaomin Wei Yunwei Dong Pengpeng Sun Mingrui Xiao |
| author_sort | Xiaomin Wei |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-11T13:57:31Z |
| format | Article |
| id | doaj.art-e43bc31a9cfe4082ab613dd32164afe5 |
| institution | Directory Open Access Journal |
| issn | 2079-9292 |
| language | English |
| last_indexed | 2024-04-11T13:57:31Z |
| publishDate | 2019-02-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Electronics |
| spelling | doaj.art-e43bc31a9cfe4082ab613dd32164afe52022-12-22T04:20:13ZengMDPI AGElectronics2079-92922019-02-018221210.3390/electronics8020212electronics8020212Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic GamesXiaomin Wei0Yunwei Dong1Pengpeng Sun2Mingrui Xiao3School of Computer Science and Engineering, Northwestern Polytechnical University, Xi’an 710072, ChinaSchool of Computer Science and Engineering, Northwestern Polytechnical University, Xi’an 710072, ChinaSchool of Computer Science and Engineering, Northwestern Polytechnical University, Xi’an 710072, ChinaSchool of Computer Science and Engineering, Northwestern Polytechnical University, Xi’an 710072, ChinaAs 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.https://www.mdpi.com/2079-9292/8/2/212safety analysisAADLgrid cyber-physical systemsmodel-checking of stochastic games |
| spellingShingle | Xiaomin Wei Yunwei Dong Pengpeng Sun Mingrui Xiao Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games Electronics safety analysis AADL grid cyber-physical systems model-checking of stochastic games |
| title | Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games |
| title_full | Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games |
| title_fullStr | Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games |
| title_full_unstemmed | Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games |
| title_short | Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games |
| title_sort | safety analysis of aadl models for grid cyber physical systems via model checking of stochastic games |
| topic | safety analysis AADL grid cyber-physical systems model-checking of stochastic games |
| url | https://www.mdpi.com/2079-9292/8/2/212 |
| work_keys_str_mv | AT xiaominwei safetyanalysisofaadlmodelsforgridcyberphysicalsystemsviamodelcheckingofstochasticgames AT yunweidong safetyanalysisofaadlmodelsforgridcyberphysicalsystemsviamodelcheckingofstochasticgames AT pengpengsun safetyanalysisofaadlmodelsforgridcyberphysicalsystemsviamodelcheckingofstochasticgames AT mingruixiao safetyanalysisofaadlmodelsforgridcyberphysicalsystemsviamodelcheckingofstochasticgames |