Projekte pro Jahr
Abstract
The use of formal methods to prove the correctness of compositional embedded systems is increasingly important. However, the required models and algorithms can induce an enormous complexity. Our approach divides the formal system model into layers and these in turn into modules with defined interfaces, so that reduced formal models can be created for the verification of concrete functional and non-functional requirements. In this work, we use Uppaal to (1) model an RTOS kernel in a modular way and formally specify its internal requirements, (2) model abstract tasks that trigger all kernel functionalities in all combinations or scenarios, and (3) verify the resulting system with regard to task synchronization, resource management, and timing. The result is a fully verified model of the operating system layer that can henceforth serve as a dependable foundation for verifying compositional applications w.r.t. various aspects, such as timing or liveness.
Originalsprache | englisch |
---|---|
Titel | Fundamental Approaches to Software Engineering - 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings |
Untertitel | International Conference on Fundamental Approaches to Software Engineering |
Redakteure/-innen | Leen Lambers, Sebastián Uchitel, Sebastián Uchitel |
Erscheinungsort | Cham |
Herausgeber (Verlag) | Springer |
Seiten | 26-46 |
Seitenumfang | 21 |
ISBN (Print) | 978-3-031-30825-3 |
DOIs | |
Publikationsstatus | Veröffentlicht - Apr. 2023 |
Veranstaltung | 26th International Conference on Fundamental Approaches to Software Engineering: FASE 2023 - Paris, Frankreich Dauer: 20 Apr. 2023 → 27 Apr. 2023 |
Publikationsreihe
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Band | 13991 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (elektronisch) | 1611-3349 |
Konferenz
Konferenz | 26th International Conference on Fundamental Approaches to Software Engineering |
---|---|
Kurztitel | FASE |
Land/Gebiet | Frankreich |
Ort | Paris |
Zeitraum | 20/04/23 → 27/04/23 |
ASJC Scopus subject areas
- Theoretische Informatik
- Allgemeine Computerwissenschaft
Fields of Expertise
- Information, Communication & Computing
Fingerprint
Untersuchen Sie die Forschungsthemen von „A Modeling Concept for Formal Verification of OS-Based Compositional Software“. Zusammen bilden sie einen einzigartigen Fingerprint.-
CompEAS-BSW1 - Kompositorische eingebettete Fahrzeugsysteme - Basissoftware
Baunach, M. C., Manjunath, V., Nagarajan, D. & Krisper, M.
1/11/20 → 31/03/25
Projekt: Forschungsprojekt
-
Verlaesslichkeit im Internet der Dinge
Boano, C. A., Kubin, G., Bloem, R., Horn, M., Pernkopf, F., Zakany, N., Mangard, S., Witrisal, K., Römer, K. U., Aichernig, B., Bösch, W., Baunach, M. C., Tappler, M., Malenko, M., Weiser, S., Eichlseder, M., Leitinger, E., Grosinger, J., Großwindhager, B., Ebrahimi, M., Alothman Alterkawi, A. B., Knoll, C., Teschl, R., Saukh, O., Rath, M., Steinberger, M., Steinbauer-Wagner, G. & Tranninger, M.
1/01/16 → 31/03/22
Projekt: Forschungsprojekt
-
Betriebssysteme für eingebettete Systeme
Baunach, M. C., Martins Gomes, R., Batista Ribeiro, L., Malenko, M., Mauroner, F. & Scheipel, T. P.
1/09/15 → 31/12/23
Projekt: Forschungsprojekt