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)  can be formulated in our framework. (C) 2009 Elsevier B.V. All rights reserved.
|Autori:||De Francesco N; Lettieri G; Martini L; Vaglini G|
|Titolo:||Partial model checking via abstract interpretation|
|Anno del prodotto:||2010|
|Digital Object Identifier (DOI):||10.1016/j.ipl.2009.10.014|
|Appare nelle tipologie:||1.1 Articolo in rivista|