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

We are concerned in this paperwith the verification of reactive systems with event memorization.The reactive systems are specified with an asynchronous reactivelanguage Electre the main feature of whichis the capability of memorizing occurrences of events in orderto process them later. This memory capability is quite interestingfor specifying reactive systems but leads to a verification modelwith a dramatically large number of states (due to the storedoccurrences of events). In this paper, we show that partial-ordermethods can be applied successfuly for verification purposeson our model of reactive programs with event memorization. Themain points of our work are two-fold: (1) we show that the independencerelation which is a key point for applying partial-order methodscan be extracted automatically from an Electreprogram; (2) the partial-order technique turns out to be veryefficient and may lead to a drastic reduction in the number ofstates of the model as demonstrated by a real-life industrialcase study.