Sciweavers

Share
IPL
2010

Partial model checking via abstract interpretation

8 years 6 months ago
Partial model checking via abstract interpretation
model checking via abstract interpretation N. De Francesco, G. Lettieri∗ , L. Martini, G. Vaglini Universit`a di Pisa, Dipartimento di Ingegneria dell’Informazione, sez. Informatica, Via Diotisalvi 2, 56122 Pisa, Italy 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 interpretation framework to reason about this problem in a systematic way. Given P and L, the set of all transition systems that, composed with stricted 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 [1] can be formulated in our framework. Key words: Compositional verification, Te...
Nicoletta De Francesco, Giuseppe Lettieri, Luca Ma
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where IPL
Authors Nicoletta De Francesco, Giuseppe Lettieri, Luca Martini, Gigliola Vaglini
Comments (0)
books