Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Abdelouahed ZAKARI Connect in order to contact the contributor
Submitted on : Friday, August 20, 2021 - 10:28:24 AM
Last modification on : Saturday, August 21, 2021 - 3:06:49 AM




Lamia Eljadiri, Ismail Assayad, Abdelouahed 2018 Zakari. Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions. International Conference on Smart Digital Environement 18-20 october 2018 Rabat, Morocco conf. ACM SIGAPP, Oct 2018, Rabat, Morocco. pp.166-171, ⟨10.1145/3289100.3289127⟩. ⟨hal-03234423⟩



Record views