Abstract
The increasing complexity of safety-critical systems and the shorter time-to-market requires a high degree of automation during all development phases from requirements specification to design, implementation, verification, and safety assurance. To make this feasible, we need to describe different system aspects using appropriate models that are semantically rich and, whenever possible, formally defined such that they are verifiable by automated methods. At the same time, they must be easy to understand by practitioners and must allow them to capture the domain concepts with minimal encoding bias. In this chapter, we describe FASTEN, an open-source research environment for model-based specification and design of safety-critical systems using domain-specific languages. FASTEN enables the experimentation with modeling abstractions at different levels of rigor and their integration in today’s development processes. We present an overview of the currently available domain-specific languages (DSLs) used to formally specify requirements, system designs, and assurance arguments. These DSLs have been developed and used in technology transfer projects by researchers from different organizations—Siemens, Bosch, fortiss, and itemis. Last but not least, we discuss lessons learned from implementing the languages and interacting with practitioners and discuss the language engineering features of MPS that enabled our approach and its open challenges.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abele, A.: Transformation of a state description into a qualitative fault tree. In: Praxisforum Fehlerbaumanalyse & Co. (2019)
Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., Tang, A.: Aligning qualitative, real-time, and probabilistic property specification patterns using a structured english grammar. IEEE Trans. Software Eng. 41(7), 620–638 (2015)
Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.G.: Contracts for systems design: Theory. Tech. rep., INRIA (2015)
Bozzano, M., Munk, P., Schweizer, M., Tonetta, S., Vozárová, V.: Model-based safety analysis of mode transitions. In: Proc. of SAFECOMP (2020)
Cârlan, C., Ratiu, D.: FASTEN.Safe: A model-driven engineering tool to experiment with checkable assurance cases. In: Proceedings of the International Conference on Computer Safety, Reliability, and Security (SAFECOMP), LNCS, vol. 12234, pp. 298–306. Springer (2020)
Cawley, O., Wang, X., Richardson, I.: Lean/agile software development methodologies in regulated environments - state of the art. In: Proceedings of First International Conference on Lean Enterprise Software and Systems - LESS, Lecture Notes in Business Information Processing, vol. 65, pp. 31–36. Springer (2010)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification, CAV ’02, pp. 359–364. Springer, Berlin, Heidelberg (2002)
Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: 38th Euromicro Conference on Software Engineering and Advanced Applications, SEAA 2012, Cesme, Izmir, Turkey, September 5–8, 2012, pp. 21–28 (2012)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), Lecture Notes in Computer Science. Springer (2004)
De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, p. 337–340. Springer, Berlin, Heidelberg (2008)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE ’99, p. 411–420. Association for Computing Machinery, New York, NY, USA (1999)
Erdweg, S., Van Der Storm, T., Völter, M., Boersma, M., Bosman, R., Cook, W.R., Gerritsen, A., Hulshout, A., Kelly, S., Loh, A., et al.: The state of the art in language workbenches. In: International Conference on Software Language Engineering, pp. 197–217. Springer (2013)
Graydon, P.J.: Formal assurance arguments: A solution in search of a problem? In: 2015 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, pp. 517–528 (2015). https://doi.org/10.1109/DSN.2015.28
Hatcliff, J., Wassyng, A., Kelly, T., Comar, C., Jones, P.: Certifiably safe software-dependent systems: Challenges and directions. In: Future of Software Engineering Proceedings, FOSE 2014, pp. 182–200. Association for Computing Machinery, New York, NY, USA (2014)
Holzmann, G.: Spin Model Checker, the: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003)
ISO: 26262: Road vehicles-Functional safety, vol. 26262. International Organisation for Standardization (ISO) (2018)
Kaiser, B., Weber, R., Oertel, M., Böde, E., Nejad, B.M., Zander, J.: Contract-based design of embedded systems integrating nominal behavior and safety. Complex Syst. Inf. Model. Q. (CSIMQ) 4, 66–91 (2015)
Kelly, T., Weaver, R.: The goal structuring notation – a safety argument notation. In: Proc. of Dependable Systems and Networks 2004 Workshop on Assurance Cases (2004)
Knight, J.: Fundamentals of Dependable Computing for Software Engineers. CRC Press (2012)
Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: 27th International Conference on Software Engineering (ICSE 2005), 15–21 May 2005, St. Louis, Missouri, USA, pp. 372–381 (2005)
Kossak, F., Mashkoor, A., Geist, V., Illibauer, C.: Improving the understandability of formal specifications: An experience report. In: Salinesi, C., van de Weerd, I. (eds.) Requirements Engineering: Foundation for Software Quality, pp. 184–199. Springer International Publishing, Cham (2014)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV’11), LNCS, vol. 6806, pp. 585–591. Springer (2011)
Leveson, N.: Engineering a Safer World, 1st edn. MIT Press (2012)
Leveson, N.G., Thomas, J.P.: Stpa Handbook. Cambridge, MA, USA (2018)
Munk, P., Nordmann, A.: Model-based safety assessment with SysML and component fault trees: application and lessons learned. Software Syst. Model. 19, 889–910 (2020)
Nordmann, A., Munk, P.: Lessons learned from model-based safety assessment with SysML and component fault trees. In: Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2018, pp. 134–143. ACM (2018)
OMG: OMG Systems Modeling Language (OMG SysML), Version 1.3 (2012). http://www.omg.org/spec/SysML/1.3/
Post, A., Menzel, I., Hoenicke, J., Podelski, A.: Automotive behavioral requirements expressed in a specification pattern system: a case study at Bosch. Requirements Engineering 17(1), 19–33 (2012)
Ratiu, D., Gario, M., Schoenhaar, H.: FASTEN: An open extensible framework to experiment with formal specification approaches. In: Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE ’19, pp. 41–50. IEEE Press (2019)
Rauhut, J.: Safety assurance of open context systems. Master’s thesis, University of Applied Science Esslingen (2020)
Spichkova, M., Zamansky, A.: Teaching of formal methods for software engineering. In: Proceedings of the 11th International Conference on Evaluation of Novel Software Approaches to Software Engineering - Volume 1: COLAFORM, (ENASE), pp. 370–376. SciTePress (2016)
The Assurance Case Working Group: Goal structuring notation community standard version 2 (2018). https://scsc.uk/scsc-141B
Tommila, T., Pakonen, A.: Controlled natural language requirements in the design and analysis of safety critical i & c systems. Tech. rep., VTT, Finland (2014)
Viger, T., Salay, R., Selim, G.M.K., Chechik, M.: Just enough formality in assurance argument structures. In: Computer Safety, Reliability, and Security - 39th International Conference, SAFECOMP 2020, Lisbon, Portugal, September 16–18, 2020, Proceedings, Lecture Notes in Computer Science. Springer (2020)
Voelter, M., Ratiu, D., Kolb, B., Schaetz, B.: mbeddr: Instantiating a language workbench in the embedded software domain. Automat. Software Eng. 20(3), 339–390 (2013)
Voelter, M., Szabó, T., Lisson, S., Kolb, B., Erdweg, S., Berger, T.: Efficient development of consistent projectional editors using grammar cells. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering, SLE 2016, pp. 28–40. ACM (2016)
Völter, M., Kolb, B., Birken, K., Tomassetti, F., Alff, P., Wiart, L., Wortmann, A., Nordmann, A.: Using language workbenches and domain-specific languages for safety-critical software development. Software Syst. Model. 18, 2507–2530 (2018)
Voelter, M., Birken, K., Lisson, S., Rimer, A.: Shadow models: Incremental transformations for MPS. In: Proceedings of the 12th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2019, pp. 61–65. ACM (2019)
Vuori, M.: Agile development of safety-critical software. Tech. rep., Tampere University of Technology. Department of Software Systems. Report 14 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Ratiu, D., Nordmann, A., Munk, P., Carlan, C., Voelter, M. (2021). FASTEN: An Extensible Platform to Experiment with Rigorous Modeling of Safety-Critical Systems. In: Bucchiarone, A., Cicchetti, A., Ciccozzi, F., Pierantonio, A. (eds) Domain-Specific Languages in Practice. Springer, Cham. https://doi.org/10.1007/978-3-030-73758-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-73758-0_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-73757-3
Online ISBN: 978-3-030-73758-0
eBook Packages: Computer ScienceComputer Science (R0)