Development of a Meta-language and its Qualifiable Implementation for the Use in Safety-critical Software

TL;DR

This paper presents a new meta-language framework based on UML and Ada SPARK for developing safety-critical software, aiming to reduce certification effort and improve correctness assurance in domain-specific modeling.

Contribution

It introduces a qualifiable meta-language and runtime environment tailored for safety-critical systems, integrating multi-level modeling and formal verification features.

Findings

Framework enables certifiable domain-specific modeling

Reduces manual certification effort

Supports formal verification with Ada SPARK

Abstract

The use of domain-specific modeling for development of complex (cyber-physical) systems is gaining increasing acceptance in the industrial environment. Domain-specific modeling allows complex systems and data to be abstracted for a more efficient system design, development, validation, and configuration. However, no existing (meta-)modeling framework can be used with reasonable effort in certified software so far, neither for the development of systems nor for the execution of system functions. For the use of (development) artifacts from domain-specific modeling in safety-critical processes or systems it is required to ensure their correctness by either subsequent (manual) verification or the usage of (pre-)qualified software. Existing meta-languages often contain modeling elements that are difficult or impossible to implement in a qualifiable manner leading to a high manual, subsequent certification effort. Therefore, the aim is to develop a (meta-)modeling framework, that can be used in certified software. This can significantly reduce the development effort for safety-critical systems and enables the full advantages of domain-specific modeling. The framework components considered in this PhD-Thesis include: (1) an essential meta-language, (2) a qualifiable runtime environment, and (3) a suitable persistence. The essential \mbox{(meta-)}modeling language is mainly based on the UML standard, but is enhanced with multi-level modeling concepts such as deep instantiation. Supporting a possible qualification, the meta-language is implemented using the highly restrictive, but formally provable programming language Ada SPARK.