Natural Projection as Partial Model Checking
- PDF / 1,271,232 Bytes
- 37 Pages / 439.37 x 666.142 pts Page_size
- 63 Downloads / 195 Views
Natural Projection as Partial Model Checking Gabriele Costa1 Chiara Bodei2
· Letterio Galletta1 · Pierpaolo Degano2 · David Basin3 ·
Received: 22 June 2020 / Accepted: 26 June 2020 © The Author(s) 2020
Abstract Verifying the correctness of a system as a whole requires establishing that it satisfies a global specification. When it does not, it would be helpful to determine which modules are incorrect. As a consequence, specification decomposition is a relevant problem from both a theoretical and practical point of view. Until now, specification decomposition has been independently addressed by the control theory and verification communities through natural projection and partial model checking, respectively. We prove that natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. Apart from their foundational interest, our results build a bridge whereby the control theory community can reuse algorithms and results developed by the verification community. Furthermore, we extend the notions of natural projection and partial model checking from finite-state to symbolic transition systems and we show that the equivalence still holds. Symbolic transition systems are more expressive than traditional finite-state transition systems, as they can model large systems, whose behavior depends on the data handled, and not only on the control flow. Finally, we present an algorithm for the partial model checking of both kinds of systems that can be used as an alternative to natural projection. Keywords Natural projection · Partial evaluation · Formal verification · Model checking
B
Gabriele Costa [email protected] Letterio Galletta [email protected] Pierpaolo Degano [email protected] David Basin [email protected] Chiara Bodei [email protected]
1
SysMA Unit, IMT School for Advanced Studies, Lucca, Italy
2
Department of Informatics, Università di Pisa, Pisa, Italy
3
Department of Computer Science, ETH Zurich, Zurich, Switzerland
123
G. Costa et al.
1 Introduction System verification requires comparing a system’s behavior against a specification. When the system is built from several components, we can distinguish between local and global specifications. A local specification applies to a single component, whereas a global specification should hold for the entire system. Since these two kinds of specifications are used to reason at different levels of abstraction, both kinds are often needed. Ideally one aims at freely passing from local to global specifications and vice versa. Most specification formalisms natively support specification composition and there are wellstudied examples of operators for composing them, e.g., logical conjunction, set intersection, and the synchronous product of automata. Unfortunately, the same does not hold for specification decomposition: obtaining local specifications from a global one is, in general, much more difficult. Over the past decades, many research communities have independently investigated decomposi
Data Loading...
