Formal Verification of Concurrent Embedded Software - Embedded Systems: Design, Analysis and Verification Access content directly
Conference Papers Year : 2013

Formal Verification of Concurrent Embedded Software


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.
Fichier principal
Vignette du fichier
978-3-642-38853-8_20_Chapter.pdf (194.5 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01466676 , version 1 (13-02-2017)





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⟩
282 View
158 Download



Gmail Facebook X LinkedIn More