Charles André, Robert de Simone
Complex reactive behaviours can be expressed by synchronous imperative formalisms like Esterel or SyncCharts. To make the best of these models and to avoid the pitfall of “causality cycles”, the user has to understand the underlying semantics, known as the “constructive semantics”. The first part of this paper is an informal introduction to this semantics. In the second part, this semantics is used to analyze “intra-instant properties” (partial ordering of simultaneous action executions). It appears that the compiler, which implements the constructive semantics, can carry out such analyses. Our method is illustrated by a zFIFO (0 fall-through time FIFO queue), which is a system envolving numerous simultaneous actions whose execution order may be critical.
reactive systems, synchrony, ESTEREL, SYNCCHARTS, constructive semantics, model checking.
@ARTICLE{sp:jesa2002,
AUTHOR = "Charles Andr\'e and Robert {De Simone}",
TITLE = "Synchronous Programming : Properties within a Reaction",
JOURNAL = "JESA",
sorte= "revue" ,
YEAR = {2002},
VOLUME = {36},
NUMBER = {7},
PAGES = {891--903}
}