טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentDisenfeld Cynthia
SubjectCompositional Verification of Events and Responses
DepartmentDepartment of Computer Science
Supervisor Professor Shmuel Katz
Full Thesis textFull thesis text - English Version


Abstract

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. Event detectors are only allowed to observe the system to indicate when something of interest occurs, while responses may change the system state or control flow, or cause other events to be detected.

In this work, we show how under a set of assumptions, the model to verify a response in hierarchical event-based systems is formally represented as the parallel composition of the response and event detectors.  We allow responses to be activated within other responses and present the extended specification and necessary proof obligations to verify, detect interference and check cooperation among responses under this scenario. Moreover, we describe how some other possible assumptions affect the formal model and proof obligations.

Counterexample-guided Abstraction Refinement (CEGAR [Clarke et al 2000]) is an iterative algorithm for considering at each verification step an abstraction of the system, and refining the abstraction when a spurious counterexample is obtained (the counterexample is consistent with the abstract model but not with the concrete version of the system).

We have introduced a CEGAR-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. This technique makes the proof obligations for modular verification, interference detection and cooperation checking more feasible in practice. Our CEGAR-based technique considers only the relevant event specifications, and learns only a part of their specifications as assumptions.

Whenever a spurious counterexample is found (i.e., the abstract counterexample to a complex event detector guarantee, response guarantee or interference proof obligation is not consistent with the lower-level event specifications), our technique modularly finds the necessary refinements that induce state splitting to avoid the counterexample automatically. Eventually, either verification succeeds or a real counterexample is found. In addition, new techniques are presented for more feasible spuriousness checking of counterexamples of liveness response guarantees, and to avoid including unnecessary parts of the event detector alphabet in the model of a response.

We have implemented these ideas in a tool (DaVeRS) and evaluated the techniques in three extensive case studies.