%0 Conference Proceedings
%T Parametric Statistical Model Checking of UAV Flight Plan
%+ PIXIEL GROUP
%+ Laboratoire des Sciences du Numérique de Nantes (LS2N)
%A Bao, Ran
%A Attiogbe, Christian
%A Delahaye, Benoit
%A Fournier, Paulin
%A Lime, Didier
%Z Part 1: Full Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Copenhagen, Denmark
%Y Jorge A. Pérez
%Y Nobuko Yoshida
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-11535
%P 57-74
%8 2019-06-17
%D 2019
%R 10.1007/978-3-030-21759-4_4
%K UAV
%K Formal model
%K Markov chain
%K Parametric statistical model checking
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Unmanned Aerial Vehicles (UAV) are now widespread in our society and are often used in a context where they can put people at risk. Studying their reliability, in particular in the context of flight above a crowd, thus becomes a necessity. In this paper, we study the modeling and analysis of UAV in the context of their flight plan. To this purpose, we build a parametric probabilistic model of the UAV and use it, as well as a given flight plan, in order to model its trajectory. This model takes into account parameters such as potential filter or sensor (like GPS) failure as well as wind force and direction. Because of the nature and complexity of the successive obtained models, their exact verification using tools such as PRISM or PARAM is impossible. We therefore develop a new approximation method, called Parametric Statistical Model Checking, in order to compute failure probabilities. This method has been implemented in a prototype tool, which we use to resolve complex issues in a practical case study.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02313737/document
%2 https://inria.hal.science/hal-02313737/file/478668_1_En_4_Chapter.pdf
%L hal-02313737
%U https://inria.hal.science/hal-02313737
%~ UNIV-NANTES
%~ INSTITUT-TELECOM
%~ CNRS
%~ EC-NANTES
%~ UNAM
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ LS2N
%~ LS2N-AELOS
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-11535
%~ INSTITUTS-TELECOM
%~ NANTES-UNIVERSITE
%~ UNIV-NANTES-AV2022
%~ NU-CENTRALE