Projects per year
The increasing dependability requirements and hardware diversity of the Internet of Things (IoT) pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for Real Time Operating Systems (RTOSs), automatic porting for all current and future devices will also be required. As part of our framework for embedded RTOS portability, based on formal methods and code generation, we present our approach to formally model low-level operating-system functionality using Event-B. We show the part of our RTOS model where the switch into the kernel and back to a task happens, and prove that the model is correct according to the specification. Hardware details are only introduced in late refinements, which allows us to reuse most of the RTOS model and proofs for several target platforms. As a proof of concept, we refine the generic model to two different architectures and prove safety and liveness properties of the models.
|Title of host publication||Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings|
|Subtitle of host publication||18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings|
|Editors||Frank de Boer, Antonio Cerone|
|Number of pages||20|
|Publication status||Published - 2020|
|Event||18th International Conference on Software Engineering and Formal Methods: SEFM 2020 - Virtuell, Amsterdam, Netherlands|
Duration: 14 Sep 2020 → 18 Sep 2020
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||18th International Conference on Software Engineering and Formal Methods|
|Abbreviated title||SEFM 2020|
|Period||14/09/20 → 18/09/20|
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Fields of Expertise
- Information, Communication & Computing
FingerprintDive into the research topics of 'A Formal Modeling Approach for Portable Low-Level OS Functionality'. Together they form a unique fingerprint.
- 4 Active
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
Project: Research project