@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}
}

{"_id":"ejRCZAAPpLMg5SyhT","authorIDs":["55095a39df05089b6e000283"],"author_short":["Herbreteau, F.","Cassez, F.","Roux, O."],"bibbaseid":"herbreteau-cassez-roux-applicationofpartialordermethodstoreactivesystemswitheventmemorization-2001","bibdata":{"bibtype":"article","type":"article","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 \\emphindependance 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":[{"propositions":[],"lastnames":["Herbreteau"],"firstnames":["Frédéric"],"suffixes":[]},{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"propositions":[],"lastnames":["Roux"],"firstnames":["Olivier"],"suffixes":[]}],"category":"langrt","journal":"Journal of Real-Time Systems","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","bibtex":"@ARTICLE{herbreteau-jrts-01,\n ABSTRACT = {We are concerned in this paper with the verification of\n reactive systems with event memorization. The\n reactive systems are specified with an asynchronous\n reactive language {\\sf Electre} the main feature of\n which is the capability of memorizing occurrences of\n events in order to process them later. This memory\n capability is quite interesting for specifying\n reactive systems but leads to a verification model\n with a dramatically large number of states (due to\n the stored occurrences of events). In this paper, we\n show that {\\em partial-order} methods can be applied\n successfuly for verification purposes on our model\n of reactive programs with event memorization. The\n main points of our work are two-fold: (1) we show\n that the \\emph{independance relation} which is a key\n point for applying partial-order methods can be\n extracted automatically from an {\\sf Electre}\n program; (2) the partial-order technique turns out\n to be very efficient and may lead to a drastic\n reduction in the number of states of the model as\n demonstrated by a real-life industrial case study. },\n AUTHOR = {Herbreteau, Fr\\'ed\\'eric and Franck Cassez and Roux, Olivier},\n CATEGORY = {langrt},\n JOURNAL = JRTS,\n MONTH = MAY,\n PUBLISHER = KLUWER,\n CLASS = {internatjournal},\n LEX = {A},\n NUMBER = {3},\n NUMIRCYN = {A},\n PAGES = {287-316},\n PDF = {./ps-pdf-files/jrts-01.pdf},\n PS = {./ps-pdf-files/jrts-01.ps.gz},\n TITLE = {{Application of Partial-Order Methods to Reactive Systems with Event Memorization}},\n VOLUME = {20},\n YEAR = {2001}\n}\n\n","author_short":["Herbreteau, F.","Cassez, F.","Roux, O."],"key":"herbreteau-jrts-01","id":"herbreteau-jrts-01","bibbaseid":"herbreteau-cassez-roux-applicationofpartialordermethodstoreactivesystemswitheventmemorization-2001","role":"author","urls":{},"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/mabib.bib","creationDate":"2015-03-18T11:11:41.221Z","downloads":0,"keywords":[],"search_terms":["application","partial","order","methods","reactive","systems","event","memorization","herbreteau","cassez","roux"],"title":"Application of Partial-Order Methods to Reactive Systems with Event Memorization","year":2001,"dataSources":["yYF8uwWqay28JyxZC"]}