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.
Type de document :
Communication dans un congrès
Gunar Schirner; Marcelo Götz; Achim Rettberg; Mauro C. Zanella; Franz J. Rammig. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. Springer, IFIP Advances in Information and Communication Technology, AICT-403, pp.218-227, 2013, Embedded Systems: Design, Analysis and Verification. 〈10.1007/978-3-642-38853-8_20〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01466676
Contributeur : Hal Ifip <>
Soumis le : lundi 13 février 2017 - 16:38:46
Dernière modification le : vendredi 1 décembre 2017 - 01:09:41
Document(s) archivé(s) le : dimanche 14 mai 2017 - 15:03:05

Fichier

978-3-642-38853-8_20_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Dirk Nowotka, Johannes Traub. Formal Verification of Concurrent Embedded Software. Gunar Schirner; Marcelo Götz; Achim Rettberg; Mauro C. Zanella; Franz J. Rammig. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. Springer, IFIP Advances in Information and Communication Technology, AICT-403, pp.218-227, 2013, Embedded Systems: Design, Analysis and Verification. 〈10.1007/978-3-642-38853-8_20〉. 〈hal-01466676〉

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

57