Application of partial-order methods to reactive programs with event memorization

Frédéric Herbreteau*, Franck Cassez, Olivier Roux

*Corresponding author for this work

Research output: Contribution to journalArticle

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 independence relation which is a key point for applying partial-order methods can be extracted automatically from an Electro 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.

Original languageEnglish
Pages (from-to)287-316
Number of pages30
JournalReal-Time Systems
Volume20
Issue number3
DOIs
Publication statusPublished - May 2001
Externally publishedYes

Keywords

  • Composition
  • Event memorizing
  • Partial-order methods
  • Reactive languages
  • Transition systems

Fingerprint Dive into the research topics of 'Application of partial-order methods to reactive programs with event memorization'. Together they form a unique fingerprint.

  • Cite this