Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions
Abstract
Formal verification plays an important role in the area of embedded systems design and in the verification of critical systems. It can reveal common errors and check complex properties defined by temporal logic formulas. To reduce the time-to-market for embedded systems design and assist Sys-temC designers in the complexity of the verification process of various systems prototypes, we propose a novel approach for generic verification of safety properties for SystemC programs. In that approach, programs models are built uppon an automata based framework such that incomplete interactions are kept, which makes the produced models composable with future programs without any changes except for the set of priorities over interactions. These compositional forms enable to check safety properties for each SystemC program once at design time, without the need for the designers to execute the verification process every time these programs are involved in the creation of new prototypes. We present the verification approach and show its feasibility.