A framework for verification of SystemC designs using SystemC waiting state automata

Nesrine Harrath; Bruno Monsuez; Kamel Barkaoui

doi:10.1007/978-3-319-04717-1_4

A framework for verification of SystemC designs using SystemC waiting state automata

Nesrine Harrath, Bruno Monsuez, Kamel Barkaoui

Conservatoire National des Arts et Métiers

Research output: Contribution to journal › Article › peer-review

Abstract

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 chapter, 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. Finally, we define how to apply model checking to prove the correctness of the abstract analysis.

Original language	English
Pages (from-to)	77-104
Number of pages	28
Journal	Advances in Intelligent Systems and Computing
Volume	263
DOIs	https://doi.org/10.1007/978-3-319-04717-1_4
Publication status	Published - 1 Jan 2014

Keywords

Automata
Formal verification
Model checking
Predicate abstraction
Symbolic execution
SystemC

Access to Document

10.1007/978-3-319-04717-1_4

Cite this

@article{cc916ca4ad77435883be67d646a0a1b3,

title = "A framework for verification of SystemC designs using SystemC waiting state automata",

abstract = "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 chapter, 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. Finally, we define how to apply model checking to prove the correctness of the abstract analysis.",

keywords = "Automata, Formal verification, Model checking, Predicate abstraction, Symbolic execution, SystemC",

author = "Nesrine Harrath and Bruno Monsuez and Kamel Barkaoui",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2014.",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-319-04717-1\_4",

language = "English",

volume = "263",

pages = "77--104",

journal = "Advances in Intelligent Systems and Computing",

issn = "2194-5357",

}

TY - JOUR

T1 - A framework for verification of SystemC designs using SystemC waiting state automata

AU - Harrath, Nesrine

AU - Monsuez, Bruno

AU - Barkaoui, Kamel

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2014.

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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 chapter, 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. Finally, we define how to apply model checking to prove the correctness of the abstract analysis.

AB - 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 chapter, 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. Finally, we define how to apply model checking to prove the correctness of the abstract analysis.

KW - Automata

KW - Formal verification

KW - Model checking

KW - Predicate abstraction

KW - Symbolic execution

KW - SystemC

U2 - 10.1007/978-3-319-04717-1_4

DO - 10.1007/978-3-319-04717-1_4

M3 - Article

AN - SCOPUS:84912082580

SN - 2194-5357

VL - 263

SP - 77

EP - 104

JO - Advances in Intelligent Systems and Computing

JF - Advances in Intelligent Systems and Computing

ER -

A framework for verification of SystemC designs using SystemC waiting state automata

Abstract

Keywords

Access to Document

Fingerprint

Cite this