A formally defined and formally provable EBNF-based constraint language for use in qualifiable software
V. Tietz, und B. Annighoefer. Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, Seite 862–871. New York, NY, USA, Association for Computing Machinery, (09.11.2022)
DOI: 10.1145/3550356.3561552
Zusammenfassung
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.
%0 Conference Paper
%1 Tietz2022
%A Tietz, Vanessa
%A Annighoefer, Bjoern
%B Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings
%C New York, NY, USA
%D 2022
%I Association for Computing Machinery
%K myown
%P 862–871
%R 10.1145/3550356.3561552
%T A formally defined and formally provable EBNF-based constraint language for use in qualifiable software
%U https://doi.org/10.1145/3550356.3561552
%X 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.
%@ 9781450394673
@inproceedings{Tietz2022,
abstract = {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.},
added-at = {2023-02-02T09:35:32.000+0100},
address = {New York, NY, USA},
author = {Tietz, Vanessa and Annighoefer, Bjoern},
biburl = {https://puma.ub.uni-stuttgart.de/bibtex/2ad1327c18b5665f3fa962a86cbf722cd/vtietz},
booktitle = {Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings},
day = 9,
doi = {10.1145/3550356.3561552},
interhash = {2e6ffec23edabb712a67d2d06f827877},
intrahash = {ad1327c18b5665f3fa962a86cbf722cd},
isbn = {9781450394673},
keywords = {myown},
location = {Montreal, Quebec, Canada},
month = {11},
pages = {862–871},
publisher = {Association for Computing Machinery},
series = {MODELS '22},
timestamp = {2023-02-02T08:53:24.000+0100},
title = {A formally defined and formally provable EBNF-based constraint language for use in qualifiable software},
url = {https://doi.org/10.1145/3550356.3561552},
year = 2022
}