The Taub Faculty of Computer Science Events and Talks

In reactive systems, responses react to interesting occurrences (events). Event detectors allow detecting complex events by gathering information and hierarchically composing lower-level event detectors. In this work, we introduce a CEGAR (Counterexample Guided Abstraction Refinement)-based compositional verification technique for verifying complex event detectors and response guarantees and finding the necessary assumptions of the response specification about lower-level event detectors in hierarchical event-based systems. Moreover, we consider the scenario where responses cause new events to be detected (thus making other responses activated). We extend the proof obligations necessary for modular verification and interference detection to allow this scenario. We have implemented these ideas in a tool (DaVeRS) and evaluated the techniques in three extensive case studies.