Final Semantics for Event-Pattern Reactive Programs
Event-pattern reactive programs are front-end programs for
distributed reactive components that preprocess an incoming stream
of event stimuli. Their purpose is to recognize temporal patterns of
events that are relevant to the serviced program and ignore all
other events, outsourcing some of the component's complexity and
shielding it from event overload. Correctness of event-pattern
reactive programs is essential, because bugs may result in loss of
relevant events and hence failure to react appropriately.
We introduce \PAR, a specification language for event-pattern
reactive programs. We propose a new approach for defining such
languages in terms of observations and actions. This approach
applies standard techniques from coalgebra to obtain instances of
the corecursion and coinduction principles. Corecursion is used to
formally define the operational semantics of \PAR, and coinduction
allows to prove general equivalences between (ground and
parameterized)
\PAR programs.
This is the first of a series of papers in which we study questions of expressive completeness, complexity, and formal verification techniques for specification languages of event-pattern reactive programs.
