Nowadays the emphasis in software engineering research is on the evolution of preexisting 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 phi. 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 phi, is modeled as the abstract semantics of phi, parametric with respect to P and L. We show that the algorithm developed by Andersen (1995) [1] can be formulated in our framework. (C) 2009 Elsevier B.V. All rights reserved.
Partial model checking via abstract interpretation
DE FRANCESCO, NICOLETTA;LETTIERI, GIUSEPPE;VAGLINI, GIGLIOLA
2010-01-01
Abstract
Nowadays the emphasis in software engineering research is on the evolution of preexisting 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 phi. 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 phi, is modeled as the abstract semantics of phi, parametric with respect to P and L. We show that the algorithm developed by Andersen (1995) [1] can be formulated in our framework. (C) 2009 Elsevier B.V. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
