Deifel, H.-P.; Dietrich, C.; Göttlinger, M.; Milius, S.; Lohmann, D.; Schröder, L.: Automatic Verification of Application-Tailored OSEK Kernels. In: Formal Methods in Computer Aided Design (FMCAD), 2017, S. 196-203. DOI: http://dx.doi.org/10.23919/FMCAD.2017.8102260
Zusammenfassung: | |
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. | |
Lizenzbestimmungen: | Es gilt deutsches Urheberrecht. Das Dokument darf zum eigenen Gebrauch kostenfrei genutzt, aber nicht im Internet bereitgestellt oder an Außenstehende weitergegeben werden. |
Publikationstyp: | ConferenceObject |
Publikationsstatus: | acceptedVersion |
Erstveröffentlichung: | 2017-08-08 |
Die Publikation erscheint in Sammlung(en): | Fakultät für Elektrotechnik und Informatik |
Pos. | Land | Downloads | ||
---|---|---|---|---|
Anzahl | Proz. | |||
1 | Germany | 129 | 53,31% | |
2 | United States | 44 | 18,18% | |
3 | France | 18 | 7,44% | |
4 | Japan | 8 | 3,31% | |
5 | China | 8 | 3,31% | |
6 | United Kingdom | 5 | 2,07% | |
7 | Korea, Republic of | 3 | 1,24% | |
8 | Czech Republic | 3 | 1,24% | |
9 | Ireland | 2 | 0,83% | |
10 | Indonesia | 2 | 0,83% | |
andere | 20 | 8,26% |
Hinweis
Zur Erhebung der Downloadstatistiken kommen entsprechend dem „COUNTER Code of Practice for e-Resources“ international anerkannte Regeln und Normen zur Anwendung. COUNTER ist eine internationale Non-Profit-Organisation, in der Bibliotheksverbände, Datenbankanbieter und Verlage gemeinsam an Standards zur Erhebung, Speicherung und Verarbeitung von Nutzungsdaten elektronischer Ressourcen arbeiten, welche so Objektivität und Vergleichbarkeit gewährleisten sollen. Es werden hierbei ausschließlich Zugriffe auf die entsprechenden Volltexte ausgewertet, keine Aufrufe der Website an sich.