Application of Partial-Order Methods to Reactive Systems with Event Memorization

Abstract : We are concerned in this paper with the verification of reactive systems with event memorization. The reactive systems are specified with an asynchronous reactive language Electre the main feature of which is the capability of memorizing occurrences of events in order to process them later. This memory capability is quite interesting for specifying reactive systems but leads to a verification model with a dramatically large number of states (due to the stored occurrences of events). In this paper, we show that partial-order methods can be applied successfuly for verification purposes on our model of reactive programs with event memorization. The main points of our work are two-fold: (1) we show that the independance relation which is a key point for applying partial-order methods can be extracted automatically from an \sf Electre program; (2) the partial-order technique turns out to be very efficient and may lead to a drastic reduction in the number of states of the model as demonstrated by a real-life industrial case study.
Type de document :
Article dans une revue
Journal of Real-Time Systems, Kluwer, 2001, 20 (3), pp.287-316
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00363027
Contributeur : Franck Cassez <>
Soumis le : vendredi 20 février 2009 - 01:04:22
Dernière modification le : mercredi 16 mai 2018 - 11:48:04
Document(s) archivé(s) le : mardi 8 juin 2010 - 22:44:26

Fichier

jrts-01.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00363027, version 1

Citation

Frédéric Herbreteau, Franck Cassez, Olivier Roux. Application of Partial-Order Methods to Reactive Systems with Event Memorization. Journal of Real-Time Systems, Kluwer, 2001, 20 (3), pp.287-316. 〈inria-00363027〉

Partager

Métriques

Consultations de la notice

471

Téléchargements de fichiers

117