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 ...

• Type: Conference
• Year: 2005
• Where: CALCO
• Authors: César Sánchez, Henny B. Sipma, Matteo Slanina, Zohar Manna
• Keywords: CALCO 2005, Event-pattern Reactive Programs, Reactive Components, Specification Languages