Formal verification of a safety argumentation and application to a complex UAV system

In the context of safety-critical systems, arguing that the system is acceptably safe is a major issue, in particular when facing a certification process. We are developing an approach which aims at providing assurance that safety objectives are met by a system under development. We propose a language to express a safety argumentation together with a semantic definition on which an implementation is based. The ultimate objective is to have means to decide, at the level of requirements, the correctness of an argumentation using a formal and tool supported approach. In this paper, we illustrate our argumentation framework on the problem of safe insertion of Unmanned Aerial Vehicle (UAV) into the air traffic. The system we consider is a socio-technical organization, which consists of the UAV control systems, and the air traffic management. The support environment built upon existing tools is briefly described.