Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Virtual Prototyping of Embedded Systems: Speed and Accuracy Tradeoffs Read chapter Read first chapter

2017 | OriginalPaper | Chapter

6. Formal Methods for Aerospace Systems

Achievements and Challenges

Authors : Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta

Published in: Cyber-Physical System Design from an Architecture Analysis Viewpoint

Publisher: Springer Singapore

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The size and complexity of control software in aerospace systems is rapidly increasing, and this development complicates its validation within the context of the overall spacecraft system. Classical validation methods are both labour intensive and error prone as they rely on manual analysis, review and inspection. Thus there is a growing trend to incorporate the use of automated formal methods. This chapter introduces the ESA-funded COMPASS project, which aims at an integrated system-software co-engineering approach focusing on a coherent set of specification and analysis techniques for evaluation of system-level correctness, safety, dependability and performability of on-board computer-based aerospace systems. Its modelling features and supporting toolset provide a unifying framework for system validation, employing state-of-the-art temporal-logic model checking techniques for infinite-state transition systems, both qualitative and probabilistic, with extensions to fault detection, identification and recovery (FDIR) and safety analysis. We provide an overview of the technology and of the results that have been achieved so far, and address several challenges for future developments. Current efforts of the project consortium concentrate on improving and advancing both process as well as technology of the COMPASS approach, with the goal of bringing the methods to higher levels of technology readiness.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Combined Model Checking and Testing Create Confidence—A Case on Commercial Automotive Operating System
Literature
1.
S. Abdelwahed, G. Karsai, N. Mahadevan, S. Ofsthun, Practical implementation of diagnosis systems using timed failure propagation graph models. IEEE Trans. Instrum. Meas. 58(2), 240–247 (2009)CrossRef
2.
E. Alaña, H. Naranjo, Y. Yushtein, M. Bozzano, A. Cimatti, M. Gario, R. de Ferluc, G. Garcia, Automated generation of FDIR for the COMPASS integrated toolset (AUTOGEF), in Proceedings of DASIA 2012, vol. ESA SP 701 (2012)
3.
J. Alonso, M. Grottke, A.P. Nikora, K.S. Trivedi, An empirical investigation of fault repairs and mitigations in space mission system software, in Proceedings of DSN 2013 (IEEE, 2013), pp. 1–8
4.
5.
M. Autili, L. Grunske, M. Lumpe, P. Pelliccione, A. Tang, Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar. IEEE Trans. Software Eng. 41(7), 620–638 (2015)CrossRef
6.
C. Baier, B. Haverkort, H. Hermanns, J.P. Katoen, Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)CrossRefMATH
7.
C. Baier, B.R. Haverkort, H. Hermanns, J.P. Katoen, Model checking meets performance evaluation. SIGMETRICS Perform. Eval. Rev. 32(4), 10–15 (2005)CrossRefMATH
8.
C. Baier, J.P. Katoen, Principles of Model Checking (MIT Press, New York, 2008)MATH
9.
E. Bartocci, R. Grosu, P. Katsaros, C.R. Ramakrishnan, S.A. Smolka, Model repair for probabilistic systems, in Proceedings of TACAS 2011. LNCS, vol. 6605 (Springer, 2011), pp. 326–340
10.
A. Biere, A. Cimatti, E. Clarke, Y. Zhu, Symbolic model checking without BDDs, in Proceedings of TACAS 1999. LNCS, vol. 1579 (Springer, 1999), pp. 193–207
11.
A. Biere, K. Heljanko, T.A. Junttila, T. Latvala, V. Schuppan, Linear encodings of bounded LTL model checking. Logical Methods Comput. Sci. 2(5) (2006)
12.
B. Bittner, Formal failure analyses for effective fault management: an aerospace perspective, Ph.D. thesis, University of Trento, 2016
13.
B. Bittner, M. Bozzano, R. Cavada, A. Cimatti, M. Gario, A. Griggio, C. Mattarei, A. Micheli, G. Zampedri, The xSAP safety analysis platform, in Proceedings of TACAS 2016. LNCS, vol. 9636 (Springer, 2016), pp. 533–539
14.
B. Bittner, M. Bozzano, A. Cimatti, Automated synthesis of timed failure propagation graphs, in Proceedings of IJCAI 2016 (AAAI Press, 2016), pp. 972–978
15.
B. Bittner, M. Bozzano, A. Cimatti, R. de Ferluc, M. Gario, A. Guiotto, Y. Yushtein, An integrated process for FDIR design in aerospace, in Proceedings of IMBSA 2014. LNCS, vol. 8822 (Springer, 2014), pp. 82–95
16.
B. Bittner, M. Bozzano, A. Cimatti, X. Olive, Symbolic synthesis of observability requirements for diagnosability, in Proceedings of AAAI-12 (2012)
17.
B. Bittner, M. Bozzano, A. Cimatti, G. Zampedri, Automated verification and tightening of failure propagation models, in Proceedings of AAAI 2016 (2016), pp. 3724–3730
18.
V. Bos, H. Bruintjes, S. Tonetta, Catalogue of system and software properties, in Proceedings of SAFECOMP 2016. LNCS, vol. 9922 (Springer, 2016), pp. 88–101
19.
H. Boudali, P. Crouzen, M. Stoelinga, A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Secure Comput. 7(2), 128–143 (2010)CrossRef
20.
M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Schulz, R. Sebastiani, Mathsat: tight integration of SAT and mathematical decision procedures. J. Autom. Reason. 35, 265–293 (2005)MathSciNetCrossRefMATH
21.
M. Bozzano, A. Cimatti, M. Gario, A. Micheli, SMT-based validation of timed failure propagation graphs, in Proceedings of AAAI 2015 (2015), pp. 3724–3730
22.
M. Bozzano, A. Cimatti, M. Gario, S. Tonetta, Formal design of fault detection and identification components using temporal epistemic logic, in Proceedings of TACAS 2014. LNCS, vol. 8413 (Springer, 2014), pp. 46–61
23.
M. Bozzano, A. Cimatti, M. Gario, S. Tonetta, Formal design of asynchronous fault detection and identification components using temporal epistemic logic. Logical Methods Comput. Sci. 11(4), 1–33 (2015)MathSciNetCrossRefMATH
24.
M. Bozzano, A. Cimatti, J.P. Katoen, P. Katsaros, K. Mokos, V.Y. Nguyen, T. Noll, B. Postma, M. Roveri, Spacecraft early design validation using formal methods. Reliab. Eng. Syst. Safety 132, 20–35 (2014)CrossRef
25.
M. Bozzano, A. Cimatti, J.P. Katoen, V.Y. Nguyen, T. Noll, M. Roveri, Safety, dependability, and performance analysis of extended AADL models. Comput. J. 54(5), 754–775 (2011)CrossRef
26.
M. Bozzano, A. Cimatti, C. Mattarei, A. Griggio, Efficient anytime techniques for model-based safety analysis, in Proceedings of CAV 2015. LNCS, vol. 9206 (Springer, 2015), pp. 603–621
27.
M. Bozzano, A. Cimatti, C. Mattarei, S. Tonetta, Formal safety assessment via contract-based design, in Proceedings of ATVA 2014 (2014), pp. 81–97
28.
M. Bozzano, A. Cimatti, F. Tapparo, Symbolic fault tree analysis for reactive systems, in Proceedings of ATVA 2007. LNCS, vol. 4762 (Springer, 2007), pp. 162–176
29.
T. Brázdil, V. Forejt, J. Kretínský, A. Kucera, The satisfiability problem for Probabilistic CTL, in Proceedings of LICS 2008 (IEEE, 2008), pp. 391–402
30.
M. Broy, B. Jonsson, J.P. Katoen, M. Leucker, A. Pretschner, (eds.), Model-Based Testing of Reactive Systems: Advanced Lectures. LNCS, Vol. 3472 (Springer, 2005)
31.
H. Bruintjes, J.P. Katoen, D. Lesens, A statistical approach for timed reachability in AADL models, in Proceedings of DSN 2015 (IEEE CS Press, 2015), pp. 81–88
32.
R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, S. Tonetta, The nuXmv symbolic model checker. CAV 2014, 334–342 (2014)
33.
S. Chakraborty, J.P. Katoen, On the satisfiability of some simple probabilistic logics, in Proceedings of LICS 2016 (ACM, 2016), pp. 56–66
34.
A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV 2: an open-source tool for symbolic model checking, in Proceedings of CAV 2002. LNCS, vol. 2404 (Springer, 2002), pp. 359–364
35.
A. Cimatti, R. Demasi, S. Tonetta, Tightening a contract refinement, in Proceedings of SEFM 2016 (2016), pp. 386–402
36.
A. Cimatti, M. Dorigatti, S. Tonetta, OCRA: a tool for checking the refinement of temporal contracts, in Proceedings of ASE 2013 (2013), pp. 702–705
37.
A. Cimatti, C. Pecheur, R. Cavada, Formal verification of diagnosability via symbolic model checking, in Proceedings of IJCAI 2003 (Morgan Kaufmann, 2003), pp. 363–369
38.
A. Cimatti, S. Tonetta, Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333–348 (2015)CrossRef
39.
40.
41.
42.
C. Dehnert, S. Junges, N. Jansen, F. Corzilius, M. Volk, H. Bruintjes, J.P. Katoen, E. Abraham, PROPhESY: a probabilistic parameter synthesis tool, in Proceedings of CAV 2015, LNCS, vol. 9206 (Springer, 2015), pp. 214–231
43.
44.
Software considerations in airborne systems and equipment certification. Software Standard DO-178C/ED-12C, RTCA Inc. and EUROCAE (2011)
45.
J.B. Dugan, S.J. Bavuso, M.A. Boyd, Dynamic fault-tree models for fault-tolerant computer systems. IEEE Trans. Reliab. 41(3), 363–377 (1992)CrossRefMATH
46.
M. Dwyer, G. Avrunin, J. Corbett, Patterns in property specifications for finite-state verification, in Proceedings of ICSE 1999 (IEEE CS Press, 1999), pp. 411–420
47.
Space engineering: Verification. ECSS Standard E-ST-10-02C, European Cooperation for Space Standardization (2009)
48.
Space engineering: System engineering general requirements. ECSS Standard E-ST-10C, European Cooperation for Space Standardization (2009)
49.
Space product assurance: Failure modes, effects (and criticality) analysis (FMEA/FMECA). ECSS Standard Q-ST-30-02C, European Cooperation for Space Standardization (2009)
50.
Space product assurance: Availability analysis. ECSS Standard Q-ST-30-09C, European Cooperation for Space Standardization (2008)
51.
Space product assurance: Dependability. ECSS Standard Q-ST-30C, European Cooperation for Space Standardization (2009)
52.
Space product assurance: Fault tree analysis—adoption notice ECSS/IEC 61025. ECSS Standard Q-ST-40-12C, European Cooperation for Space Standardization (2008)
53.
Space product assurance: Safety. ECSS Standard Q-ST-40C, European Cooperation for Space Standardization (2009)
54.
M.A. Esteve, J.P. Katoen, V.Y. Nguyen, B. Postma, Y. Yushtein, Formal correctness, safety, dependability and performance analysis of a satellite, in Proceedings of ICSE 2012 (ACM and IEEE CS Press, 2012), pp. 1022–1031
55.
K. Etessami, M.Z. Kwiatkowska, M.Y. Vardi, M. Yannakakis, Multi-objective model checking of Markov decision processes. Logical Methods Comput. Sci. 4(4) (2008)
56.
V. Forejt, M. Kwiatkowska, D. Parker, Pareto curves for probabilistic model checking, in Proceedings of ATVA 2012. LNCS, vol. 7561 (Springer, 2012), pp. 317–332
57.
58.
D. Guck, T. Han, J.P. Katoen, M.R. Neuhäußer, Quantitative timed analysis of interactive Markov chains, in Proceedings of NFM 2012. LNCS, vol. 7226 (Springer, 2012), pp. 8–23
59.
D. Guck, H. Hatefi, H. Hermanns, J.P. Katoen, M. Timmer, Modelling, reduction and analysis of Markov automata, in Proceedings of QEST 2013. LNCS, vol. 8054 (Springer, 2013), pp. 55–71
60.
K. Heljanko, T.A. Junttila, T. Latvala, Incremental and complete bounded model checking for full PLTL, in Proceedings of CAV 2005. LNCS, vol. 3576 (2005), pp. 98–111
61.
H. Hermanns, Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428 (Springer, 2002)
62.
G.J. Holzmann, The power of 10: rules for developing safety-critical code. Computer 39(6), 95–99 (2006)CrossRef
63.
N. Jansen, F. Corzilius, M. Volk, R. Wimmer, E. Abraham, J.P. Katoen, B. Becker, Accelerating parametric probabilistic verification, in Proceedings of QEST 2014. LNCS, vol. 8657 (Springer, 2014), pp. 404–420
64.
S. Junges, D. Guck, J.P. Katoen, A. Rensink, M. Stoelinga, Fault trees on a diet, in Proceedings of SETTA 2015. LNCS, vol. 9409 (Springer, 2015), pp. 3–18
65.
J.P. Katoen, V.Y. Nguyen, T. Noll, Formal validation methods in model-based spacecraft systems engineering, in Modeling and Simulation-Based Systems Engineering Handbook, Chap. 14 (CRC Press, 2014), pp. 339–375
66.
J.P. Katoen, L. Song, L. Zhang, Probably safe or live, in Proceedings of CSL-LICS 2014 (ACM, 2014), pp. 55:1–55:10
67.
J.P. Katoen, I.S. Zapreev, E.M. Hahn, H. Hermanns, D.N. Jansen, The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)CrossRef
68.
M. Kwiatkowska, G. Norman, D. Parker, H. Qu, Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38–65 (2013)MathSciNetCrossRefMATH
69.
70.
A. Misra, J. Sztipanovits, A. Underbrink, R. Carnes, B. Purves, Diagnosability of dynamical systems, in 3rd International Workshop on Principles of Diagnosis (1992), pp. 239–244
71.
72.
T. Noll, Safety, dependability and performance analysis of aerospace systems, in Proceedings of FTSCS 2014. CCIS, vol. 476 (Springer, 2015), pp. 17–31
73.
74.
75.
76.
S.C. Ofsthun, S. Abdelwahed, Practical applications of timed failure propagation graphs for vehicle diagnosis, in Proceedings of Autotestcon 2007 (IEEE, 2007), pp. 250–259
77.
S. Pathak, E. Abraham, N. Jansen, A. Tacchella, J.P. Katoen, A greedy approach for the efficient repair of stochastic models, in Proceedings of NFM 2015. LNCS, vol. 9058 (Springer, 2015), pp. 295–309
78.
M. Perrotin, E. Conquet, J. Delange, A. Schiele, T. Tsiodras, TASTE: a real-time software engineering tool-chain overview, status, and future, in Proceedings of SDL 2011. LNCS, vol. 7083 (Springer, 2012), pp. 26–37
79.
I. Pill, S. Semprini, R. Cavada, M. Roveri, R. Bloem, A. Cimatti, Formal analysis of hardware requirements, in Proceedings of DAC 2006 (2006), pp. 821–826
80.
81.
Architecture Analysis & Design Language (AADL) Annex, Volume 1, Annex E: Error Model Annex. SAE Standard AS5506/1A (International Society of Automotive Engineers, 2015)
82.
Architecture Analysis and Design Language (AADL) Annex, Volume 1, Annex A: Graphical AADL Notation. SAE Standard AS5506/1 (International Society of Automotive Engineers, 2006)
83.
Architecture Analysis & Design Language (AADL). SAE Standard AS5506 (International Society of Automotive Engineers, 2004)
84.
Architecture Analysis & Design Language (AADL) (rev. B). SAE Standard AS5506B (International Society of Automotive Engineers, 2012)
85.
86.
A. Valmari, G. Franceschinis, Simple \(O(m \log n)\) time Markov chain lumping, in Proceedings of TACAS 2010. LNCS, vol. 6015 (Springer, 2010), pp. 38–52
87.
M. Volk, S. Junges, J.P. Katoen, Advancing dynamic fault tree analysis – get succinct state spaces fast and synthesise failure rates, in Proceedings of SAFECOMP 2016. LNCS, vol. 9922 (Springer, 2016), pp. 253–265
88.
R. Wimmer, M. Herbstritt, H. Hermanns, K. Strampp, B. Becker, Sigref – a symbolic bisimulation tool box, in Proceedings of ATVA 2006. LNCS, vol. 4218 (Springer, 2006), pp. 477–492
Metadata
Title
Formal Methods for Aerospace Systems
Authors
Marco Bozzano
Harold Bruintjes
Alessandro Cimatti
Joost-Pieter Katoen
Thomas Noll
Stefano Tonetta
Copyright Year
2017
Publisher
Springer Singapore
Book
Cyber-Physical System Design from an Architecture Analysis Viewpoint

Print ISBN: 978-981-10-4435-9

Electronic ISBN: 978-981-10-4436-6

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-981-10-4436-6_6

Premium Partner

    Image Credits