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 metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01466676
Contributor : Hal Ifip <>
Submitted on : Monday, February 13, 2017 - 4:38:46 PM
Last modification on : Friday, December 1, 2017 - 1:09:41 AM
Long-term archiving on : Sunday, May 14, 2017 - 3:03:05 PM

File

978-3-642-38853-8_20_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

195

Files downloads

198