@InCollection{PassaSant:2021:AiNaSy,
               author = "Passa, Gabriel Duarte and Santiago J{\'u}nior, Valdivino 
                         Alexandre de",
                title = "Aircraft Navigation Systems Safety Assessment via Probabilistic 
                         Model Checking",
            booktitle = "Computational Science and its Applications (ICCSA) 2021",
            publisher = "Springer",
                 year = "2021",
               editor = "Gervasi, O. and Murgante, B. and Misra, S. and Garau, C. and 
                         Blecic, I. and Apduhan, B. O. and Rocha, A. M. A. C. and 
                         Tarantino, E. and Torre, C. M.",
                pages = "465--480",
             keywords = "Aerospace systems, Aircraft navigation, Probabilistic model 
                         checking, Safety assessment.",
             abstract = "The safety assessment process is a mandatory step in the 
                         development and certification of safety-critical systems such as 
                         the ones in the aerospace industry. In this work we show how 
                         Probabilistic Model Checking, a Formal Verification method, can 
                         help to assess the safety of navigation systems for a civil 
                         commercial transport category aircraft. The process involves a 
                         top-down approach identifying functions and its respective failure 
                         modes. Each failure event is associated with a hazard level, with 
                         an inverse relationship between the maximum acceptable probability 
                         and the event severity. Fault Tree Analysis (FTA) is the most 
                         commonly used method to quantify each events probability, but 
                         probabilistic models are also accepted as means of compliance 
                         demonstration, as per ARP-4761. Results show that the use of 
                         Probabilistic Model Checking as a means to complement non-formal 
                         methods is valuable, where we were able to evaluate the 
                         probability of several failure modes described in FAAs AC 20-138D, 
                         making use of Continuous-Time Markov Chains (CTMCs) with up 4.3 
                         million of reachable states and 60 million of transitions.",
          affiliation = "{} and {Instituto Nacional de Pesquisas Espaciais (INPE)}",
                  doi = "10.1007/978-3-030-86973-1_33",
                  url = "http://dx.doi.org/10.1007/978-3-030-86973-1_33",
                 isbn = "978-303086972-4",
             language = "en",
           targetfile = "Pasa_Santiago Jr_ICCSA 2021_Vers{\~a}o Autor.pdf",
               volume = "12952",
        urlaccessdate = "21 maio 2024"
}