Reactive Systems with Unbounded Event Memorization

Abstract:

In this paper, we study an infinite state machine designed for the modelling of the behaviors of reactive systems with event memorization. Starting from an Electre program, we show how to compute a FIFFO (First In First Fireable Out) transition system modelling the memorizing and the processing of memorized events. All the steps of this computation are illustrated on the well-known readers-writers synchronization problem.

Keywords:

Reactive systems, Specification languages and tools, Semantics, Unbounded Memorization.

Download:

[ps.gz | pdf]

Note: the abstract of the paper is written in french, but the remaining of the paper is written in english.

BibTeX entry:

@InProceedings{CHR:CARI00, author = "Cassez, F. and Herbreteau, F. and Roux, O.", title = "Reactive Systems with Unbounded Event Memorization", booktitle = "Conf{\'e}rence Africaine de Recherche en Informatique (CARI'00)", year = "2000", month = oct, address = "Antananarivo, Madagascar", }