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...

• Type: Journal
• Year: 2010
• Where: IPL
• Authors: Nicoletta De Francesco, Giuseppe Lettieri, Luca Martini, Gigliola Vaglini
• Keywords: De Francesco, Di Pisa, IPL 2010, Pre-existing Sub-systems