zbMATH — the first resource for mathematics

Model-based safety assessment of a triple modular generator with xSAP. (English) Zbl 07349691
Summary: The system design process needs to cope with the increasing complexity and size of systems, motivating the replacement of labor intensive manual techniques with automated and semi-automated approaches. Recently, formal methods techniques, such as model-based verification and safety assessment, have been increasingly used to model systems under fault and to analyze them, generating artifacts such as fault trees and FMEA tables. In this paper, we show how to apply model-based techniques to a realistic case study from the avionics domain: a high integrity power distribution system, the Triple Modular Generator (TMG). The TMG is composed of a redundant and reconfigurable plant and a controller that must guarantee a high level of reliability. The case study is a significant challenge, from the modeling perspective, since it implements a complex reconfiguration policy, specified via a number of requirements in natural language, including a set of mutually dependent and potentially conflicting priority constraints. Moreover, from the verification standpoint, the controller must be able to handle an exponential number of possible faulty configurations. Our contribution is twofold. First, we formalize and validate the requirements and, using a constraint-based modeling style, we synthesize a correct by construction controller, avoiding the enumeration of all possible fault configurations, as is currently done by manual approaches. Second, we describe a comprehensive methodology and process, supported by the xSAP safety analysis platform that targets the modeling and safety assessment of faulty systems. Using xSAP, we are able to automatically extract minimal cut sets for the TMG. We demonstrate the scalability of our approach by analyzing a parametric version of the TMG case study that contains more than 700 variables and 90 faults.
68-XX Computer science
MCK; nuXmv; Simulink; NuSMV
Full Text: DOI
[1] Akerlund O, Bieber P, Böde E, Bozzano M, Bretschneider M, Castel C, Cavallo A, Cifaldi M, Gauthier J, Griffault A, Lisagor O, Ludtke A, Metge S, Papadopoulos C, Peikenkamp T, Sagaspe L, Seguin C, Trivedi H, Valacca L (2006) ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects. In: Proceedings of the ERTS. Tolouse
[2] Abdulla, PA; Deneux, J.; Stålmarck, G.; Ågren, H.; Åkerlund, O.; Margaria, Tiziana; Steffen, Bernhard, Designing Safe, Reliable Systems Using Scade, In: Leveraging applications of formal methods, first international symposium, ISoLA 2004, Paphos, Cyprus, October 30-November 2, 2004, revised selected papers, 115-129 (2004), Springer
[3] Allen, EE; van Leeuwen, J., Temporal and modal logic, Handbook of theoretical computer science, 995-1072 (1990), Elsevier · Zbl 0900.03030
[4] Joshi A, Heimdahl MPR (2005) Model-Based Safety Analysis of Simulink Models Using SCADE Design Verifier. In: Winther R, Gran BA, Dahll G (eds) Proceedings of the computer safety, reliability, and security, 24th international conference, SAFECOMP 2005, Fredrikstad, Norway, September 28-30, 2005, volume 3688 of lecture notes in computer science. Springer, pp 122-135
[5] Alaña E, Naranjo H, Yushtein Y, Bozzano M, Cimatti A, Gario M, de Ferluc R, Garcia G (2012) Automated generation of FDIR for the compass integrated toolset (AUTOGEF). In: em DASIA, volume ESA SP 701
[6] Banach, R.; Bozzano, M., The mechanical generation of fault trees for reactive systems via retrenchment I: combinational circuits, FAC, 25, 4, 573-607 (2013) · Zbl 1298.68050
[7] Banach, R.; Bozzano, M., The mechanical generation of fault trees for reactive systems via retrenchment II: clocked and feedback circuits, FAC, 25, 4, 609-657 (2013) · Zbl 1298.68051
[8] Bittner B, Bozzano M, Cavada R, Cimatti A, Gario M, Griggio A, Mattarei C, Micheli A, Zampedri G (2016) The xSAP safety analysis platform. In: Proceedings of the TACAS, volume 9636 of LNCS, pp 533-539
[9] Bittner B, Bozzano M, Cimatti A (2017) Timed failure propagation analysis for spacecraft engineering: the ESA solar orbiter case study. In: Marco B, Yiannis P (eds) Proceedings of the model-based safety and assessment—5th international symposium, IMBSA 2017, Trento, Italy, September 11-13, 2017, volume 10437 of lecture notes in computer science. Springer, pp 255-271
[10] Bittner B, Bozzano M, Cimatti A, Olive X (2012) Symbolic synthesis of observability requirements for diagnosability. In: AAAI conference on artificial intelligence
[11] Bozzano M, Cavallo A, Cifaldi M, Valacca L, Villafiorita A (2003) Improving safety assessment of complex systems: an industrial case study. In: FME, volume 2805 of LNCS, pp. 208-222
[12] Bozzano M, Cimatti A, Gario M, Tonetta S (2014) Formal design of fault detection and identification components using temporal epistemic logic. In: Proceedings of TACAS’14, Grenoble, France, pp 326-340 · Zbl 1448.68289
[13] Bozzano, M., Cimatti, A., Gario, M., Tonetta, S.: Formal design of asynchronous fault detection and identification components using temporal epistemic logic. Log Methods Comput Sci 11(4), (2015) · Zbl 1448.68289
[14] Bozzano, M.; Cimatti, A.; Katoen, J-P; Nguyen, VY; Noll, T.; Roveri, M., Safety, dependability and performance analysis of extended aadl models, Comput J, 54, 5, 754-775 (2011)
[15] Bozzano, M.; Cimatti, A.; Katoen, J-P; Katsaros, P.; Mokos, K.; Nguyen, VY; Noll, T.; Postma, B.; Roveri, M., Spacecraft early design validation using formal methods, Rel Eng Syst Saf, 132, 20-35 (2014)
[16] Bozzano, M.; Cimatti, A.; Lisagor, O.; Mattarei, C.; Mover, S.; Roveri, M.; Tonetta, S., Safety assessment of altarica models via symbolic model checking, Sci Comput Program, 98, 4, 464-483 (2015)
[17] Bozzano, M.; Cimatti, A.; Mattarei, C., Formal reliability analysis of redundancy architectures, Formal Asp Comput, 31, 1, 59-94 (2019) · Zbl 1425.68039
[18] Bozzano M, Cimatti A, Mattarei C, Griggio A (2015) Efficient anytime techniques for model-based safety analysis. In: CAV, pp 603-621
[19] Bozzano M, Cimatti A, Mattarei C, Tonetta S (2014) Formal safety assessment via contract-based design. In: ATVA, volume 8837 of LNCS. Springer, pp 81-97 · Zbl 1448.68174
[20] Bozzano M, Cimatti A, Pires AF, Jones D, Kimberly G, Petri T, Robinson R, Tonetta S (2015) Formal design and safety analysis of AIR6110 wheel brake system. In: Proceedings of the CAV, volume 9206 of LNCS, pp 518-535
[21] Biere A, Clarke EM, Raimi R, Zhu Y (1999) Verifiying safety properties of a power PC microprocessor using symbolic model checking without BDDs. In: Halbwachs N, Peled DA (eds) Proceedings of the computer aided verification, 11th international conference, CAV ’99, Trento, Italy, July 6-10, 1999, volume 1633 of lecture notes in computer science. Springer, pp 60-71 · Zbl 1046.68578
[22] Bieber P, Castel C, Seguin C (2002) Combination of fault tree analysis and model checking for safety assessment of complex system. In: Grandoni F, Thévenod-Fosse P (eds) Proceedings of the dependable computing—EDCC-4, 4th European dependable computing conference, Toulouse, France, October 23-25, 2002, volume 2485 of lecture notes in computer science. Springer, pp 19-31
[23] Bozzano M, Cimatti A, Tapparo F (2007) Symbolic fault tree analysis for reactive systems. In: Namjoshi KS, Yoneda T, Higashino T, Okamura Y (eds) Proceedings of the automated technology for verification and analysis, 5th international symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, volume 4762 of lecture notes in computer science. Springer, pp 162-176 · Zbl 1141.68455
[24] Bouissou M (2017) A benchmark on reliability of complex discrete systems: emergency power supply of a nuclear power plant. In: Hermanns H, Höfner P (eds) Proceedings 2nd workshop on models for formal analysis of real systems, MARS@ETAPS 2017, Uppsala, Sweden, 29th April 2017, volume 244 of EPTCS, pp 200-216
[25] Bozzano, M., Causality and temporal dependencies in the design of fault management system, EPTCS, 259, 39-46 (2017)
[26] Bradley, AR; Jhala, R.; Schmidt, DA, SAT-based model checking without unrolling, VMCAI, volume 6538 of LNCS, 70-87 (2011), Springer · Zbl 1317.68109
[27] Bryant, RE, Symbolic boolean manipulation with ordered binary-decision diagrams, ACM Comput Surv, 24, 3, 293-318 (1992)
[28] Bozzano, M.; Villafiorita, A., The FSAP/NuSMV-SA safety analysis platform. STTT, 9, 1, 5-24 (2007)
[29] Bozzano M, Villafiorita A (2010) Design and safety assessment of critical systems. CRC Press (Taylor and Francis), an Auerbach Book
[30] Bozzano M, Villafiorita A, Åkerlund O et al (2003) ESACS: an integrated methodology for design and safety analysis of complex systems. In: Proceedings of the European safety and reliability conference (ESREL 2003). Balkema Publisher, pp 237-245
[31] Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In: CAV, pp 334-342
[32] Cimatti, A.; Clarke, EM; Giunchiglia, F.; Roveri, M., NuSMV: a new symbolic model checker, Softw Tools Technol Transf, 2, 4, 410-425 (2000) · Zbl 1059.68582
[33] Cavada R, Cimatti A, Mover S, Sessa M, Cadavero G, Scaglione G (2018) Analysis of relay interlocking systems via SMT-based model checking of switched multi-domain Kirchhoff networks. In: Bjørner N, Gurfinkel A (eds) 2018 formal methods in computer aided design, FMCAD 2018, Austin, TX, USA, October 30-November 2, 2018. IEEE, pp 1-9
[34] Cimatti A, Griggio A, Mover S, Tonetta S (2013) Parameter synthesis with IC3. In: Proceedings of FMCAD. IEEE, pp 165-168 · Zbl 1368.68245
[35] Cimatti A, Mover S, Sessa M (2017) SMT-based analysis of switching multi-domain linear Kirchhoff networks. In: Stewart D, Weissenbacher G (eds) 2017 formal methods in computer aided design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. IEEE, pp 188-195
[36] Cimatti A, Pecheur C, Cavada R (2003) Formal verification of diagnosability via symbolic model checking. In: Proceedings of the IJCAI, pp 363-369
[37] Cimatti, A.; Roveri, M.; Susi, A.; Tonetta, S., Validation of requirements for hybrid systems: a formal approach, ACM Trans Softw Eng Methodol, 21, 4, 22 (2012)
[38] Deneux J, Åkerlund O (2004) A common framework for design and safety analyses using formal methods. In: Conference on probabilistic safety assessment and management (PSAM7/ESREL’04)
[39] Hadjsaid, N., (2010) Novel architectures and operation modes of distribution network to increase DG integration. In: IEEE conference, general meeting, et al.: Minneapolis. IEEE, USA (2010)
[40] European cooperation on space standardization. http://www.ecss.nl
[41] Results of the electrical system dependability benchmark launched by EDF in 2017: demonstration of tools and models (2019) https://www.imdr.eu/offres/gestion/events_818_46557_non-2229/results-of-the-electrical-system-dependability-benchmark-launched-by-edf-in-2017-demonstration-of-tools-and-models.html
[42] Ezekiel J, Lomuscio A, Molnar L, Veres SM (2011) Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle. In: IJCAI, pp 1659-1664
[43] European Space Agency (2007) ESTEC ITT AO/1-5458/07NL/JD “System-software co-engineering: performance and verification”
[44] European Space Agency (2010) ESTEC ITT AO/1-6570/10/NL/LvH “Dependability design approach for critical flight software”
[45] European Space Agency (2011) ESTEC ITT AO/1-6992/11/NL/JK “FDIR development and verification & validation process”
[46] European Space Agency (2013) ESTEC ITT AO/1-7263/12/NL/AK “Hardware-software dependability for launchers”
[47] European Space Agency (2013) ESTEC ITT AO/1-7785/14/NL/MH “Catalogue of system and software properties”
[48] Guiotto A, De Ferluc R, Bozzano M, Cimatti A, Gario M, Yushtein Y (2014) Fame process: a dedicated development and V&V process for FDIR. In: Proceedings of the DASIA
[49] Gammie P, Van Der Meyden R (2004) MCK: model checking the logic of knowledge. In: CAV. Springer, pp 256-259 · Zbl 1103.68614
[50] Huang X (2013) Diagnosability in concurrent probabilistic systems. In: AAMAS, pp 853-860
[51] Halpern, JY; Vardi, MY, The complexity of reasoning about knowledge and time, Lower bounds. J Comput Syst Sci, 38, 1, 195-237 (1989) · Zbl 0672.03015
[52] Joshi A, Miller SP, Whalen M, Heimdahl MPE (2005) A proposal for model-based safety analysis. In Proceedings of the AIAA/IEEE digital avionics systems conference (DASC)
[53] Katiraei, F.; Iravani, R.; Hatziargyriou, N.; Dimeas, A., Microgrids management. IEEE Power Energy Magazine, 6, 3, 54-65 (2008)
[54] Laroussinie F, Markey N, Schnoebelen P (2002) Temporal logic with forgettable past. In: Proceedings of the 17th IEEE symposium on logic in computer science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark. IEEE Computer Society, pp 383-392
[55] Lichtenstein O, Pnueli A, Zuck L (1985) The glory of the past. In: Parikh R (ed) Logics of programs. Springer, Berlin, vol 193, pp 196-218
[56] McMillan, KL, Symbolic model checking (1993), Kluwer Academic
[57] MISSA. The MISSA Project, Last retrieved on 28 Jan 2015. http://www.missa-fp7.eu
[58] NuSMV web page (2021) https://nusmv.fbk.eu
[59] nuXmv web page (2021) https://nuxmv.fbk.eu
[60] ocra web page (2021) https://ocra.fbk.eu
[61] Papadopoulos Y (2000) Safety-directed system monitoring using safety cases. Ph.D. thesis, Department of Computer Science, University of York. Technical report YCST-2000-08
[62] Prosvirnova T, Batteux M, Brameret P-A, Cherfi A, Friedlhuber T, Roussel J-M, Rauzy A (2013) The AltaRica 3.0 project for Model-Based Safety Assessment. In: DCDS
[63] Peikenkamp T, Cavallo A, Valacca L, Böde E, Pretzer M, Hahn EM (2006) Towards a unified model-based safety assessment. In: SAFECOMP, pp 275-288
[64] Papadopoulos Y, Maruhn M (2001) Model-based synthesis of fault trees from Matlab-Simulink models. In: Proceedings of the conference on dependable systems and networks (DSN 2001), pp 77-82
[65] Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, Rhode Island, USA, 31 October-1 November 1977. IEEE Computer Society, pp 46-57
[66] Raymer DP (2018) Aircraft design: a conceptual approach, 6th edn. American Institute of Aeronautics
[67] SAE (1996) ARP4761 guidelines and methods for conducting the safety assessment process on civil airborne systems and equipment
[68] Schumann A (2004) Diagnosis of discrete-event systems using binary decision diagrams. In: Workshop on principles of diagnosis (DX’04), pp 197-202
[69] Sampath, M.; Sengupta, R.; Lafortune, S.; Sinnamohideen, K.; Teneketzis, DC, Failure diagnosis using discrete-event models, IEEE Trans Control Syst Technol, 4, 2, 105-124 (1996)
[70] Vardi MY (2001) Branching vs. linear time: final showdown. In: Margaria T, Yi W (eds) Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS’01), volume 2031 of LNCS. Springer, pp 1-22 · Zbl 0986.68064
[71] Vesely, WE; Stamatelatos, M.; Dugan, J.; Fragola, J.; Minarick, J. III; Railsback, J., Fault tree handbook with aerospace applications, 20546 (2002), NASA Headquarters, Washington, DC: Prepared for NASA Office of Safety and Mission Assurance, NASA Headquarters, Washington, DC
[72] xSAP web page (2021) https://xsap.fbk.eu
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.