Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories - Embedded Systems: Design, Analysis and Verification Access content directly
Conference Papers Year : 2013

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

Dates and versions

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

Licence

Attribution

Identifiers

Cite

Che-Wei Chang, Rainer Dömer. Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. pp.116-127, ⟨10.1007/978-3-642-38853-8_11⟩. ⟨hal-01466667⟩
89 View
66 Download

Altmetric

Share

Gmail Facebook X LinkedIn More