דלג לתוכן (מקש קיצור 's')
אירועים

אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

event speaker icon
סינטיה דיסנפלד (הרצאה סמינריונית לדוקטורט)
event date icon
יום רביעי, 31.12.2014, 11:30
event location icon
Taub 601
event speaker icon
מנחה: 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.