Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions - Université de Lorraine Accéder directement au contenu
Communication Dans Un Congrès Année : 2018

Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions

Lamia Eljadiri
  • Fonction : Auteur
  • PersonId : 1099575
Ismail Assayad
  • Fonction : Auteur
  • PersonId : 1099576

Résumé

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.
Fichier non déposé

Dates et versions

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

Identifiants

Citer

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 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More