Rechercher

[HMB13] Verifying SystemC with Predicate Abstraction: a Component Based Approach

Conférence Internationale avec comité de lecture : On the 14th International Conference on Information Reuse and Integration (IEEE IRI), August 2013, San Francisco, USA,

Mots clés: SystemC, automata, symbolic execution, predicate abstraction,formal verifi cation

Résumé: The SystemC waiting-state automaton is a compositional abstract 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 rst 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 xed points via predicate abstraction to infer relations between predicates generated during symbolic execution.

Equipe: systemes surs

BibTeX

@inproceedings {
HMB13,
title="{Verifying SystemC with Predicate Abstraction: a Component Based Approach}",
author=" N. Harrath and B. Monsuez and K. Barkaoui ",
booktitle="{On the 14th International Conference on Information Reuse and Integration (IEEE IRI)}",
year=2013,
month="August",
address="San Francisco, USA",
}