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

https://hal.univ-lorraine.fr/hal-03234423
Contributor : Abdelouahed Zakari <>
Submitted on : Friday, August 20, 2021 - 10:28:24 AM
Last modification on : Saturday, August 21, 2021 - 3:06:49 AM

Identifiers

Collections

Citation

Lamia Eljadiri, Ismail Assayad, Abdelouahed 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⟩

Share

Metrics

Record views

13