Details
| Originalsprache | Englisch |
|---|---|
| Titel des Sammelwerks | Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017) |
| Herausgeber/-innen | Georg Weissenbacher, Daryl Stewart |
| Herausgeber (Verlag) | Institute of Electrical and Electronics Engineers Inc. |
| Seiten | 196-203 |
| Seitenumfang | 8 |
| ISBN (elektronisch) | 9780983567875 |
| Publikationsstatus | Veröffentlicht - 9 Nov. 2017 |
| Veranstaltung | 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 - Vienna, Österreich Dauer: 2 Okt. 2017 → 6 Okt. 2017 |
Abstract
The OSEK industrial standard governs the design of embedded real-time operating systems in the automotive domain. We report on efforts to develop verification methods for OSEK-conformant compilers, specifically of a code generator that weaves system calls and application code using a static configuration file, producing a stand-alone application that incorporates the relevant parts of the kernel. Our methodology involves two verification steps: On the one hand, we extract an OS-application interaction graph during the compilation phase and verify that it conforms to the standard, in particular regarding prioritized scheduling and interrupt handling. To this end, we generate from the configuration file a temporal specification of standard-conformant behaviour and model check the arising formulas on a labelled transition system extracted from the interaction graph. On the other hand, we verify that the actual generated code conforms to the interaction graph; this is done by graph isomorphism checking of the interaction graph against a dynamically-explored state-transition graph of the generated system.
ASJC Scopus Sachgebiete
- Informatik (insg.)
- Theoretische Informatik und Mathematik
- Informatik (insg.)
- Computergrafik und computergestütztes Design
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017). Hrsg. / Georg Weissenbacher; Daryl Stewart. Institute of Electrical and Electronics Engineers Inc., 2017. S. 196-203 8102260.
Publikation: Beitrag in Buch/Bericht/Sammelwerk/Konferenzband › Aufsatz in Konferenzband › Forschung › Peer-Review
}
TY - GEN
T1 - Automatic Verification of Application-Tailored OSEK Kernels
AU - Deifel, Hans Peter
AU - Gottlinger, Merlin
AU - Milius, Stefan
AU - Schroder, Lutz
AU - Dietrich, Christian
AU - Lohmann, Daniel
PY - 2017/11/9
Y1 - 2017/11/9
N2 - The OSEK industrial standard governs the design of embedded real-time operating systems in the automotive domain. We report on efforts to develop verification methods for OSEK-conformant compilers, specifically of a code generator that weaves system calls and application code using a static configuration file, producing a stand-alone application that incorporates the relevant parts of the kernel. Our methodology involves two verification steps: On the one hand, we extract an OS-application interaction graph during the compilation phase and verify that it conforms to the standard, in particular regarding prioritized scheduling and interrupt handling. To this end, we generate from the configuration file a temporal specification of standard-conformant behaviour and model check the arising formulas on a labelled transition system extracted from the interaction graph. On the other hand, we verify that the actual generated code conforms to the interaction graph; this is done by graph isomorphism checking of the interaction graph against a dynamically-explored state-transition graph of the generated system.
AB - The OSEK industrial standard governs the design of embedded real-time operating systems in the automotive domain. We report on efforts to develop verification methods for OSEK-conformant compilers, specifically of a code generator that weaves system calls and application code using a static configuration file, producing a stand-alone application that incorporates the relevant parts of the kernel. Our methodology involves two verification steps: On the one hand, we extract an OS-application interaction graph during the compilation phase and verify that it conforms to the standard, in particular regarding prioritized scheduling and interrupt handling. To this end, we generate from the configuration file a temporal specification of standard-conformant behaviour and model check the arising formulas on a labelled transition system extracted from the interaction graph. On the other hand, we verify that the actual generated code conforms to the interaction graph; this is done by graph isomorphism checking of the interaction graph against a dynamically-explored state-transition graph of the generated system.
UR - http://www.scopus.com/inward/record.url?scp=85044636278&partnerID=8YFLogxK
U2 - 10.23919/FMCAD.2017.8102260
DO - 10.23919/FMCAD.2017.8102260
M3 - Conference contribution
AN - SCOPUS:85044636278
SP - 196
EP - 203
BT - Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)
A2 - Weissenbacher, Georg
A2 - Stewart, Daryl
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017
Y2 - 2 October 2017 through 6 October 2017
ER -