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

The Taub Faculty of Computer Science Events and Talks

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
event speaker icon
Advisor: Prof. Shmuel Katz
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.