Document Open Access Logo

ALPACAS: A Language for Parametric Assessment of Critical Architecture Safety

Authors Maxime Buyse, Rémi Delmas, Youssef Hamadi

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.5.pdf
  • Filesize: 1.15 MB
  • 29 pages

Document Identifiers

Author Details

Maxime Buyse
  • Uber Elevate, Paris, France
Rémi Delmas
  • Uber Elevate, Paris, France
Youssef Hamadi
  • Uber Elevate, Paris, France

Cite As Get BibTex

Maxime Buyse, Rémi Delmas, and Youssef Hamadi. ALPACAS: A Language for Parametric Assessment of Critical Architecture Safety. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 5:1-5:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ECOOP.2021.5

Abstract

This paper introduces Alpacas, a domain-specific language and algorithms aimed at architecture modeling and safety assessment for critical systems. It allows to study the effects of random and systematic faults on complex critical systems and their reliability. The underlying semantic framework of the language is Stochastic Guarded Transition Systems, for which Alpacas provides a feature-rich declarative modeling language and algorithms for symbolic analysis and Monte-Carlo simulation, allowing to compute safety indicators such as minimal cutsets and reliability. Built as a domain-specific language deeply embedded in Scala 3, Alpacas offers generic modeling capabilities and type-safety unparalleled in other existing safety assessment frameworks. This improved expressive power allows to address complex system modeling tasks, such as formalizing the architectural design space of a critical function, and exploring it to identify the most reliable variant. The features and algorithms of Alpacas are illustrated on a case study of a thrust allocation and power dispatch system for an electric vertical takeoff and landing aircraft.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Domain specific languages
  • Computer systems organization → Embedded and cyber-physical systems
Keywords
  • Domain-Specific Language
  • Deep Embedding
  • Scala 3
  • Architecture Modelling
  • Safety Assessment
  • Static Analysis
  • Monte-Carlo Methods

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Alexandre Albore, Silvano Dal Zilio, Guillaume Infantes, Christel Seguin, and Pierre Virelizier. A model-checking approach to analyse temporal failure propagation with altarica. In Marco Bozzano and Yiannis Papadopoulos, editors, Model-Based Safety and Assessment, pages 147-162, Cham, 2017. Springer International Publishing. Google Scholar
  2. R. Alur and M. Bernadsky. Bounded model checking for GSMP models of stochastic real-time systems. In J.P. Hespanha and A. Tiwari, editors, Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, volume 3927 of Lecture Notes in Computer Science, pages 19-33. Springer, 2006. URL: https://doi.org/10.1007/11730637_5.
  3. Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The essence of dependent object types. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 249-272. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_14.
  4. André Arnold, Gérald Point, Alain Griffault, and Antoine Rauzy. The altarica formalism for describing concurrent systems. Fundam. Informaticae, 40(2-3):109-124, 1999. URL: https://doi.org/10.3233/FI-1999-402302.
  5. Jonathan Bachrach, Huy Vo, Brian C. Richards, Yunsup Lee, Andrew Waterman, Rimas Avizienis, John Wawrzynek, and Krste Asanovic. Chisel: constructing hardware in a scala embedded language. In Patrick Groeneveld, Donatella Sciuto, and Soha Hassoun, editors, The 49th Annual Design Automation Conference 2012, DAC '12, San Francisco, CA, USA, June 3-7, 2012, pages 1216-1225. ACM, 2012. URL: https://doi.org/10.1145/2228360.2228584.
  6. Howard Barringer and Klaus Havelund. Tracecontract: A scala DSL for trace analysis. In Michael J. Butler and Wolfram Schulte, editors, FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings, volume 6664 of Lecture Notes in Computer Science, pages 57-72. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21437-0_7.
  7. Pierre-Marie Basset, Binh Dang Vu, Philippe Beaumier, Gabriel Reboul, and Biel Ortun. Models and methods at onera for the presizing of evtol hybrid aircraft including analysis of failure scenarios. In AHS Forum 2018, May 2018, PHOENIX, United States, 2018. Google Scholar
  8. Michel Batteux, Tatiana Prosvirnova, and Antoine Rauzy. System Structure Modeling Language (S2ML). preprint, 2015. URL: https://hal.archives-ouvertes.fr/hal-01234903.
  9. Michel Batteux, Tatiana Prosvirnova, Antoine Rauzy, and Leïla Kloul. The altarica 3.0 project for model-based safety assessment. In 11th IEEE International Conference on Industrial Informatics, INDIN 2013, Bochum, Germany, July 29-31, 2013, pages 741-746. IEEE, 2013. URL: https://doi.org/10.1109/INDIN.2013.6622976.
  10. Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. Pric3: Property directed reachability for mdps. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 of Lecture Notes in Computer Science, pages 512-538. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_27.
  11. Pierre Bieber, Remi Delmas, and Christel Seguin. Dalculus - theory and tool for development assurance level allocation. In Francesco Flammini, Sandro Bologna, and Valeria Vittorini, editors, Computer Safety, Reliability, and Security - 30th International Conference, SAFECOMP 2011, Naples, Italy, September 19-22, 2011. Proceedings, volume 6894 of Lecture Notes in Computer Science, pages 43-56. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24270-0_4.
  12. Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, and Gianni Zampedri. The xsap safety analysis platform. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 533-539. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_31.
  13. Marc Bouissou and Jean-Louis Bon. A new formalism that combines advantages of fault-trees and markov models: Boolean logic driven markov processes. Reliab. Eng. Syst. Saf., 82(2):149-163, 2003. URL: https://doi.org/10.1016/S0951-8320(03)00143-1.
  14. Marco Bozzano, Alessandro Cimatti, Alberto Griggio, and Cristian Mattarei. Efficient anytime techniques for model-based safety analysis. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 603-621. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_41.
  15. Carlos E. Budde, Pedro R. D'Argenio, and Arnd Hartmanns. Automated compositional importance splitting. Sci. Comput. Program., 174:90-108, 2019. URL: https://doi.org/10.1016/j.scico.2019.01.006.
  16. Pierre-Yves Chaux, Jean-Marc Roussel, Jean-Jacques Lesage, Gilles Deleuze, and Marc Bouissou. Systematic extraction of minimal cut sequences from a BDMP model. In 21st European Safety & Reliability Conference (ESREL 12), Jun 2012, Helsinki, Finland, 2012. Google Scholar
  17. Shengxin Dai, Mei Hong, and Bing Guo. A comparative study of reliability-ignorant and reliability-aware energy management schemes using UPPAAL-SMC. Sci. Program., 2017:2621089:1-2621089:12, 2017. URL: https://doi.org/10.1155/2017/2621089.
  18. Patrick R. Darmstadt, Ralph Catanese, Allan Beiderman, Fernando Dones, Ephraim Chen, Mihir P. Mistry, Brian Babie, Mary Beckman, , and Robin Preator. Hazards analysis and failure modes and effects criticality analysis (fmeca) of four concept vehicle propulsion systems. Technical report, NASA/Boeing, 2019. URL: https://hummingbird.arc.nasa.gov/Publications/files/CR-2019-220217.pdf.
  19. Alexandre David, Kim G Larsen, Axel Legay, Marius Mikučionis, and Danny Bøgsted Poulsen. Uppaal smc tutorial. International Journal on Software Tools for Technology Transfer, 17(4):397-415, 2015. Google Scholar
  20. Julien Delange and Peter H. Feiler. Architecture fault modeling with the AADL error-model annex. In 40th EUROMICRO Conference on Software Engineering and Advanced Applications, EUROMICRO-SEAA 2014, Verona, Italy, August 27-29, 2014, pages 361-368. IEEE Computer Society, 2014. URL: https://doi.org/10.1109/SEAA.2014.20.
  21. Kevin Delmas, Rémi Delmas, and Claire Pagetti. Smt-based architecture modelling for safety assessment. In 2017 12th IEEE International Symposium on Industrial Embedded Systems (SIES), pages 1-8. IEEE, 2017. Google Scholar
  22. Ewen Denney, Ganesh Pai, and Josef Pohl. Advocate: An assurance case automation toolset. In Frank Ortmeier and Peter Daniel, editors, Computer Safety, Reliability, and Security - SAFECOMP 2012 Workshops: Sassur, ASCoMS, DESEC4LCCI, ERCIM/EWICS, IWDE, Magdeburg, Germany, September 25-28, 2012. Proceedings, volume 7613 of Lecture Notes in Computer Science, pages 8-21. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33675-1_2.
  23. T. English and R. Heydor. Monte carlo simulation of markov, semi-markov, and generalized semi-markov processes in probabilistic risk assessment, final report. Nasa summer faculty fellowship program 2004, NASA, August 2005. Google Scholar
  24. Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, and Matthias Volk. Safety analysis for vehicle guidance systems with dynamic fault trees. Reliab. Eng. Syst. Saf., 186:37-50, 2019. URL: https://doi.org/10.1016/j.ress.2019.02.005.
  25. A. Hartmanns. MODEST - A unified language for quantitative models. In Proceeding of the 2012 Forum on Specification and Design Languages, Vienna, Austria, September 18-20, 2012, pages 44-51. IEEE, 2012. URL: http://ieeexplore.ieee.org/document/6336982/.
  26. Klaus Havelund and Rajeev Joshi. Modeling with scala. In International Symposium on Leveraging Applications of Formal Methods, pages 184-205. Springer, 2018. Google Scholar
  27. Klaus Havelund, Doron Peled, and Dogan Ulus. Dejavu: A monitoring tool for first-order temporal logic. In 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, pages 12-13. IEEE, 2018. URL: https://doi.org/10.1109/MT-CPS.2018.00013.
  28. Paul Hudak. Building domain-specific embedded languages. Acm computing surveys (csur), 28(4es):196-es, 1996. Google Scholar
  29. Cyrille Jégourel, Axel Legay, and Sean Sedwards. Importance splitting for statistical model checking rare properties. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 576-591. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_38.
  30. Sohag Kabir. An overview of fault tree analysis and its application in model based dependability analysis. Expert Systems with Applications, 77:114-135, 2017. Google Scholar
  31. Sohag Kabir, Yiannis Papadopoulos, Martin Walker, David Parker, Jose Ignacio Aizpurua, Jörg Lampe, and Erich Rüde. A model-based extension to hip-hops for dynamic fault propagation studies. In Marco Bozzano and Yiannis Papadopoulos, editors, Model-Based Safety and Assessment - 5th International Symposium, IMBSA 2017, Trento, Italy, September 11-13, 2017, Proceedings, volume 10437 of Lecture Notes in Computer Science, pages 163-178. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-64119-5_11.
  32. Shahid Khan, Joost-Pieter Katoen, and Marc Bouissou. A compositional semantics for repairable bdmps. In António Casimiro, Frank Ortmeier, Friedemann Bitsch, and Pedro Ferreira, editors, Computer Safety, Reliability, and Security - 39th International Conference, SAFECOMP 2020, Lisbon, Portugal, September 16-18, 2020, Proceedings, volume 12234 of Lecture Notes in Computer Science, pages 82-98. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-54549-9_6.
  33. Shahid Khan, Joost-Pieter Katoen, and Marc Bouissou. Explaining boolean-logic driven markov processes using gspns. In 16th European Dependable Computing Conference, EDCC 2020, Munich, Germany, September 7-10, 2020, pages 119-126. IEEE, 2020. URL: https://doi.org/10.1109/EDCC51268.2020.00028.
  34. Oleg Kiselyov. Typed tagless final interpreters. In Generic and Indexed Programming, pages 130-174. Springer, 2012. Google Scholar
  35. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM: probabilistic model checking for performance and reliability analysis. SIGMETRICS Perform. Evaluation Rev., 36(4):40-45, 2009. URL: https://doi.org/10.1145/1530873.1530882.
  36. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  37. N. Limnios and G. Oprişan. Semi-Markov Processes and Reliability. Number 1 in Statistics for Industry and Technology. Birkhäuser, Boston, MA, 2001. URL: https://doi.org/10.1007/978-1-4612-0161-8.
  38. O. Lisagor, T. Kelly, and R. Niu. Model-based safety assessment: Review of the discipline and its challenges. In The Proceedings of 2011 9th International Conference on Reliability, Maintainability and Safety, pages 625-632, 2011. URL: https://doi.org/10.1109/ICRMS.2011.5979344.
  39. Joseph Machrouh, Jean-Paul Blanquart, Philippe Baufreton, Jean-Louis Boulanger, Hervé Delseny, Jean Gassino, Gerard Ladier, Emmanuel Ledinot, Michel Leeman, Jean-Marc Astruc, Philippe Quéré, Bertrand Ricque, and Gilles Deleuze. Cross domain comparison of System Assurance. In Embedded Real Time Software and Systems (ERTS2012), Toulouse, France, 2012. URL: https://hal.archives-ouvertes.fr/hal-02170444.
  40. Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. Simplicitly: foundations and applications of implicit function types. Proc. ACM Program. Lang., 2(POPL):42:1-42:29, 2018. URL: https://doi.org/10.1145/3158130.
  41. Antoine Rauzy. Binary decision diagrams for reliability studies. In Handbook of performability engineering, pages 381-396. Springer, 2008. Google Scholar
  42. Antoine B Rauzy. Guarded transition systems: a new states/events formalism for reliability studies. Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, 222(4):495-505, 2008. Google Scholar
  43. Tiark Rompf, Nada Amin, Adriaan Moors, Philipp Haller, and Martin Odersky. Scala-virtualized: linguistic reuse for deep embeddings. High. Order Symb. Comput., 25(1):165-207, 2012. URL: https://doi.org/10.1007/s10990-013-9096-9.
  44. Tiark Rompf and Martin Odersky. Lightweight modular staging: a pragmatic approach to runtime code generation and compiled dsls. Commun. ACM, 55(6):121-130, 2012. URL: https://doi.org/10.1145/2184319.2184345.
  45. Amir Shaikhha and Lionel Parreaux. Finally, a polymorphic linear algebra language (pearl). In Alastair F. Donaldson, editor, 33rd European Conference on Object-Oriented Programming, ECOOP 2019, July 15-19, 2019, London, United Kingdom, volume 134 of LIPIcs, pages 25:1-25:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.25.
  46. Ioannis Sorokos, Luis P. Azevedo, Yiannis Papadopoulos, Martin Walker, and David J. Parker. Comparing automatic allocation of safety integrity levels in the aerospace and automotive domains. IFAC - PapersOnLine, 49(3):184-190, 2016. 14th IFAC Symposium on Control in Transportation Systems 2016. URL: https://doi.org/10.1016/j.ifacol.2016.07.031.
  47. Alain Villemeur. Reliability, availability, maintainability and safety assessment, assessment, hardware, software and human factors, volume 2. Wiley, 1992. Google Scholar
  48. Håkan L. S. Younes and Reid G. Simmons. Solving generalized semi-markov decision processes using continuous phase-type distributions. In Deborah L. McGuinness and George Ferguson, editors, Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California, USA, pages 742-748. AAAI Press / The MIT Press, 2004. URL: http://www.aaai.org/Library/AAAI/2004/aaai04-117.php.
  49. Tian Zhao and Xiaobing Huang. Design and implementation of deepdsl: A DSL for deep learning. Comput. Lang. Syst. Struct., 54:39-70, 2018. URL: https://doi.org/10.1016/j.cl.2018.04.004.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact