Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories

Abstract : For a system-on-chip design which may be composed of multiple processing elements running in parallel, improper execution order and communication assignment may lead to problematic consequences, and one of the consequences could be deadlock. In this paper, we propose an approach to abstracting SpecC-based system models for formal analysis using satisfiability modulo theories (SMT). Based on the language execution semantics, our approach abstracts the timing relations between the time intervals of the behaviors in the design. We then use a SMT solver to check if there are any conflicts among those timing relations. If a conflict is detected, our tool will read the unsatisfiable model generated by the SMT solver and report the cause of the conflict to the user. We demonstrate our approach on a JPEG encoder design model.
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.116-127, 2013, Embedded Systems: Design, Analysis and Verification. 〈10.1007/978-3-642-38853-8_11〉
Liste complète des métadonnées

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

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

Fichier

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

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Che-Wei Chang, Rainer Dömer. Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories. 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.116-127, 2013, Embedded Systems: Design, Analysis and Verification. 〈10.1007/978-3-642-38853-8_11〉. 〈hal-01466667〉

Partager

Métriques

Consultations de la notice

47

Téléchargements de fichiers

30