AltaRica and event-B models for operational safety analysis: unmanned aerial vehicle case study
Jean‐Charles Chaudemar, Eric Bensana, Charles Castel, Christel Seguin · Open Archive Toulouse Archive Ouverte (University of Toulouse) · 2009
This paper presents a method to analyse the operational safety of complex systems and the application of this method to an Unmanned Aerial Vehicle (UAV). The method relies on the complementary use of AltaRica and Event-B models. On the one hand, the AltaRica failure propagation models well support the safety analysis of complex systems. On the other hand, Event-B formalism well supports the design of system, from abstract specification to software development. Thus, the relationship between AltaRica and Event-B enables a better understanding for such a safety analysis.Accordingly, this paper focuses on the association of these two formalisms in the safety analysis of an UAV control system. This association is applied for an architecture which is structured in three hierarchical layers: operational layer, functional layer and physical equipment layer. But only the first two layers are dealt with in this paper.