HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Friday, February 20, 2009 - 1:04:22 AM
Last modification on : Wednesday, April 27, 2022 - 3:51:55 AM
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