Skip to Main content Skip to Navigation
New interface
Conference papers

Formal Verification of Concurrent Embedded Software

Abstract : With the introduction of multicore hardware to embedded systems their vulnerability to race conditions has been drastically increased. Therefore, sufficient methods and techniques have to be developed in order to identify this kind of runtime errors. In this paper, we demonstrate an approach employing a formal technique in the verification process. We use MEMICS, which is a specialized constraint solver able to identify general runtime errors as well as race conditions. We show how this tool can be embedded into an existing software analysis tool chain. In particular, we describe the process of deriving the formal input model for the solver from C code. The advantage of using constraint solving techniques is that we can offer an entire trace leading to a race condition. The ongoing development of MEMICS is part of our work inside the ARAMiS project.
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, February 13, 2017 - 4:38:46 PM
Last modification on : Thursday, March 5, 2020 - 5:40:29 PM
Long-term archiving on: : Sunday, May 14, 2017 - 3:03:05 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Dirk Nowotka, Johannes Traub. Formal Verification of Concurrent Embedded Software. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. pp.218-227, ⟨10.1007/978-3-642-38853-8_20⟩. ⟨hal-01466676⟩



Record views


Files downloads