Developing and Verifying Response Specifications in Hierarchical Event-Based Systems

We introduce a CEGAR-based compositional verification technique for verifying response guarantees and finding the necessary assumptions of the response specification about event detectors in hierarchical event-based systems. By taking advantage of the structure of such systems, only the relevant event specifications are considered, and from these only a part of their specifications is learnt as response assumptions. Whenever a spurious counterexample is found (i.e., the abstract counterexample to a response guarantee property is not consistent with the event specifications), our technique modularly finds the necessary refinements that induce state splitting and add fairness constraints to avoid the counterexample automatically. Eventually, either the response guarantee is proved 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.