Compositional reactive semantics of system-level designs written in SystemC and formal verification with predicate abstraction. (1st January 2014)

• Record Type: Journal Article
• Authors: Harrath, Nesrine; Monsuez, Bruno
• Is Part Of: International journal of critical computer-based systems. Volume 5:Number 3/4(2014)
• Page Start: 268
• Page End: 299
• Publication Date: 2014-01-01
• Subjects: SystemC -- operational semantics -- symbolic execution -- predicate abstraction -- compositional verification; Computer systems -- Periodicals; Computer architecture -- Periodicals; 004
• Languages: English
• ISSNs: 1757-8779

Abstract

In this paper, we propose a method to automatically extract an abstract representation of SystemC components into the SystemC-waiting state automata: a compositional formal model for verifying properties of SystemC at the transaction level within a delta-cycle. The main drawback of this model as mentioned in previous works was that it should be provided manually. In this paper, we propose a method to automatically build the SystemC waiting-state automata from the SystemC code. First, we select a subset of SystemC language and define its operational semantics that succinctly captures its reactive features and allows the specification of synchronous and asynchronous communications between the communicating components. Next, we symbolically execute the SystemC code using these semantics to generate the set of all possible traces and finally we use predicate abstraction to reduce the complexity of the generated graph during symbolic execution. We illustrate the use of symbolic execution and then predicate abstraction for two examples of SystemC programs: one that handles execution traces without loops and another one that handles loops.