Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [58 references]  Display  Hide  Download
Contributor : Franck Cassez <>
Submitted on : Friday, February 20, 2009 - 1:04:22 AM
Last modification on : Wednesday, December 19, 2018 - 3:02:08 PM
Long-term archiving on: : Tuesday, June 8, 2010 - 10:44:26 PM


Files produced by the author(s)


  • HAL Id : inria-00363027, version 1


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⟩



Record views


Files downloads