@ARTICLE{herbreteau-jrts-01,
  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 {\sf 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 {\em 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 \emph{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. },
  AUTHOR = {Herbreteau, Fr\'ed\'eric and Franck Cassez and Roux, Olivier},
  CATEGORY = {langrt},
  JOURNAL = JRTS,
  MONTH = MAY,
  PUBLISHER = KLUWER,
  CLASS = {internatjournal},
  LEX = {A},
  NUMBER = {3},
  NUMIRCYN = {A},
  PAGES = {287-316},
  PDF = {./ps-pdf-files/jrts-01.pdf},
  PS = {./ps-pdf-files/jrts-01.ps.gz},
  TITLE = {{Application of Partial-Order Methods to Reactive Systems with Event Memorization}},
  VOLUME = {20},
  YEAR = {2001}
}