FASTEN: An extensible platform to experiment with rigorous modeling of safety-critical systems

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.