Constructive model-based analysis for safety assessment

Autor:	Augusto Sampaio, Felipe Ferri, Alexandre Mota, Adriano Gomes, Edson Watanabe
Rok vydání:	2012
Předmět:	Soundness Fault tree analysis Markov chain Computer science Markov model computer.software_genre Constructive PRISM model checker Formal language Data mining Completeness (statistics) computer Software Information Systems
Zdroj:	International Journal on Software Tools for Technology Transfer. 14:673-702
ISSN:	1433-2787 1433-2779
DOI:	10.1007/s10009-012-0238-x
Popis:	The aerospace industry still uses fault trees to perform reliability analysis. This is because fault-tree modeling and analysis (FTA) seems easier to practical engineers when compared with Markov models, even though FTA provides a weaker form of analysis. In this paper, we propose an automatic strategy for generating Markov-based models and corresponding analysis formulations, according to ARP 4761, directly from Simulink diagrams annotated with failure information. The generated Markov-based models are expressed in the formal language PRISM, and the analysis is carried out by the PRISM model checker. The strategy is compositional and based on a comprehensive set of translation rules from Simulink to PRISM. We briefly address soundness and completeness of the rules and, to illustrate the application of the strategy, we apply it to a classical avionics case study: an actuator control system.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::db800fa6f305fdcb27054183b85c6166 https://doi.org/10.1007/s10009-012-0238-x Zobrazit plný text záznamu Full text from SpringerLink