DocumentCode
1832217
Title
Verifying SystemC with predicate abstraction: A component based approach
Author
Harrath, Nesrine ; Monsuez, Bruno ; Barkaoui, Kamel
Author_Institution
Dept. of Electron. & Comput. Eng., ENSTA ParisTech, Palaiseau, France
fYear
2013
fDate
14-16 Aug. 2013
Firstpage
536
Lastpage
545
Abstract
The SystemC waiting-state automaton is a compositional formal model for verifying properties of SystemC at the transaction level within a delta-cycle: the smallest simulation unit time in SystemC. In this paper, we first propose how to extract automata for SystemC components where we distinguish between threads and methods in SystemC. Then, we propose an approach based on a combination of symbolic execution and computing fixed points via predicate abstraction to infer relations between predicates generated during symbolic execution.
Keywords
automata theory; object-oriented programming; program verification; symbol manipulation; SystemC property verification; SystemC waiting-state automaton; component based approach; compositional formal model; delta-cycle; predicate abstraction; symbolic execution; Abstracts; Automata; Concrete; Hardware; Semantics; Sensitivity; Software;
fLanguage
English
Publisher
ieee
Conference_Titel
Information Reuse and Integration (IRI), 2013 IEEE 14th International Conference on
Conference_Location
San Francisco, CA
Type
conf
DOI
10.1109/IRI.2013.6642516
Filename
6642516
Link To Document