Skip to content (access key 's')
Logo of Technion
Logo of CS Department


Compositional Verification of Events and Responses
event speaker icon
Cynthia Disenfeld, Ph.D. Thesis Seminar
event date icon
Wednesday, 31.12.2014, 11:30
event location icon
Taub 601
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.
[Back to the index of events]