Vacuity is a leading sanity check in model-checking, applied when the system is found to satisfy the specification. The check detects situations where the specification passes in a trivial way, say when a specification that requires every request to be followed by a grant is satisfied in a system with no requests. Such situations typically reveal problems in the modelling of the system or the specification, and indeed vacuity detection is a part of most industrial model-checking tools.
Existing research and tools for vacuity concern discrete-time systems and specification formalisms. We introduce real-time vacuity, which aims to detect problems with real-time modelling. Real-time logics are used for the specification and verification of systems with a continuous-time behavior. We study vacuity for the branching real-time logic TCTL, and focus on vacuity with respect to the time constraints in the specification. Specifically, the logic TCTL includes the temporal operator \(U^J\), which specifies real-time eventualities in real-time systems: the parameter Open image in new window is an interval with integral boundaries that bounds the time in which the eventuality should hold. We define several tightenings for the \(U^J\) operator. These tightenings require the eventuality to hold within a strict subset of J. We prove that vacuity detection for TCTL is PSPACE-complete, thus it does not increase the complexity of model-checking of TCTL. Our contribution involves an extension, termed TCTL\(^+\), of TCTL, which allows the interval J not to be continuous, and for which model checking stays in PSPACE. Finally, we describe a method for ranking vacuity results according to their significance.
- 9.Chockler, H., Gurfinkel, A., Strichman, O.: Beyond vacuity: towards the strongest passing formula. In: Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design, pp. 1–8 (2008)Google Scholar
- 10.Chockler, H., Halpern, J.Y.: Responsibility and blame: a structural-model approach. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence, pp. 147–153 (2003)Google Scholar
- 13.Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proceedings of the 32st Design Automation Conference, pp. 427–432. IEEE Computer Society (1995)Google Scholar
- 16.Dokhanchi, A., Hoxha, B., Fainekos, G.E.: Formal requirement elicitation and debugging for testing and verification of cyber-physical systems. CoRR, abs/1607.02549 (2016)Google Scholar
- 23.Kupferman, O., Li, W., Seshia, S.A.: A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design, pp. 1–9 (2008)Google Scholar
- 27.Purandare, M., Wahl, T., Kroening, D.: Strengthening properties using abstraction refinement. In: Proceedings of Design, Automation and Test in Europe (DATE), pp. 1692–1697. IEEE (2009)Google Scholar