Details
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017) |
| Editors | Georg Weissenbacher, Daryl Stewart |
| Publisher | Institute of Electrical and Electronics Engineers Inc. |
| Pages | 196-203 |
| Number of pages | 8 |
| ISBN (electronic) | 9780983567875 |
| Publication status | Published - 9 Nov 2017 |
| Event | 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 - Vienna, Austria Duration: 2 Oct 2017 → 6 Oct 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 subject areas
- Computer Science(all)
- Computational Theory and Mathematics
- Computer Science(all)
- Computer Graphics and Computer-Aided Design
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017). ed. / Georg Weissenbacher; Daryl Stewart. Institute of Electrical and Electronics Engineers Inc., 2017. p. 196-203 8102260.
Research output: Chapter in book/report/conference proceeding › Conference contribution › Research › 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 -