Formal specification approaches have been successfully used to specify and verify complex systems. Verification engineers so far either use directly formal specification languages (e.g. SMV, Promela) which can be consumed by verification tools or main stream modeling languages (e.g. SysML, AADL) which are then translated into formal languages and verified. The first approach is expressive and effective but difficult to use by non-experts. The second approach lowers the entry barrier for novices but users are limited to the constructs of the chosen modeling languages and thereby end up abusing the language to encode behaviors of interest.

In this paper, we introduce a third approach that we call FASTEN, in which modular and extensible Domain Specific Languages (DSLs) are used to raise the abstraction level of specification languages towards the domain of interest. The approach aims to help novice users to use formal specification, enable experts to use multi-paradigm modeling, and provide tools to the developers of verification technologies to easily experiment with various types of specification approaches. To show the feasibility of the approach, we release an open-source tool based on Jetbrains’ MPS language workbench that provides an extensible stack of more than ten DSLs, situated at different levels of abstraction, built on top of the SMV language. We use the NuSMV model checker to perform verification, to simulate the models and lift the counterexamples at the abstraction level of the DSLs. Finally, we report on the experience of using the DSLs in practice to the study of a communication protocol of a safety critical system.