Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions - Université de Lorraine Access content directly
Conference Papers Year : 2018

Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions

Lamia Eljadiri
  • Function : Author
  • PersonId : 1099575
Ismail Assayad
  • Function : Author
  • PersonId : 1099576

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.
No file

Dates and versions

hal-03234423 , version 1 (20-08-2021)

Identifiers

Cite

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⟩
12 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More