Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Model Checking of SCADE Designed Systems

S Heim 1 Xavier Dumas 1 E Bonnafous 1 Philippe Dhaussy 2, 3 C Teodorov 2, 3 Lise Leroux 2, 3
2 Lab-STICC_ENSTAB_CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192)
3 Pôle STIC_IDM
ENSTA Bretagne - École Nationale Supérieure de Techniques Avancées Bretagne
Abstract : Model checking is a well-known method to verify a formal model in all possible configurations. Nevertheless this technique can hardly scale up to industrial asynchronous systems because of the state-space explosion problem. To address this challenge, a new approach based on context specification (the environment of the system) and an observation engine called OBP (Observer Based Prover) has been developed. The idea is that given a property to be verified, one doesn’t need to explore all possible configurations of the complete system. Among all possible behavior of the system, a tiny part is representative enough for the property to be verified. Thus, specifying a pertinent environment (a context) allows restricting the system behavior on those only parts where the property is worth verifying. The objective of our work is to apply this Context-aware verification method to the verification of SCADE systems designed in LUSTRE language, in order to check behavioral properties related to system safety. Moreover LUSTRE is a synchronous language whereas OBP exploration engine takes as input an asynchronous model designed in FIACRE language. To cope with this problem our approach consists in developing a GALS method combining asynchronous contexts with synchronous models.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01289454
Contributeur : Marc Boyer <>
Soumis le : mercredi 16 mars 2016 - 17:18:40
Dernière modification le : mercredi 24 juin 2020 - 16:19:31
Archivage à long terme le : : vendredi 17 juin 2016 - 10:56:37

Fichier

paper_9.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01289454, version 1

Citation

S Heim, Xavier Dumas, E Bonnafous, Philippe Dhaussy, C Teodorov, et al.. Model Checking of SCADE Designed Systems. 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Jan 2016, TOULOUSE, France. ⟨hal-01289454⟩

Partager

Métriques

Consultations de la notice

796

Téléchargements de fichiers

535