Partial model checking via abstract interpretation

Nowadays the emphasis in software engineering research is on the evolution of pre-existing sub-systems and component development. In this context, we tackle the following problem: given the formal specification of the system P, already built, how to characterize possible collaborators of P, through a given communication interface L, to the satisfaction of a given property φ. We propose an abstract interpretation framework to reason about this problem in a systematic way. Given P and L, the set of all transition systems that, composed with P and restricted by L, satisfy φ, is modeled as the abstract semantics of φ, parametric with respect to P and L. We show that the algorithm developed by Andersen (1995) [1] can be formulated in our framework.