A formally defined and formally provable EBNF-based constraint language for use in qualifiable software

, and . Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, page 862–871. New York, NY, USA, Association for Computing Machinery, (Nov 9, 2022)
DOI: 10.1145/3550356.3561552


In the area of domain-specific modeling, constraints play a crucial role in addition to the meta-language and meta-models, since object-based models are often not expressive enough to accurately describe real-world relations. Constraints become even more important for the use of domain-specific modeling in safety-critical areas such as avionics. By defining constraints, for example, valid value ranges can already be defined at meta-model level, thus, identifying invalid values during system and software execution. However, a constraint engine used in safety-critical software needs to be qualified and is thus subject to safety standards and regulations such as that the evaluation of constraints must not lead to undesired behavior. Therefore, a strongly restrictive constraint language which is formally defined and provable is suggested for using the full potential of domain-specific modeling in the safety-critical domain. Our new constraint language and evaluation engine is based on the safety-critical programming language Ada, operating on a meta-modeling framework additionally written in Ada, not using any object oriented features and partially verified by SPARK. The formal definition is achieved by using the Extended Backus-Naur Form (EBNF). In addition to the syntactic proof, a semantic proof of the constraint is performed based on the associated meta-model. Finally, the new constraint language is demonstrated in evaluating constraints of an avionics hardware model and meta-model all within the Ada environment.

Links and resources