HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Abstraction over Public Interfaces

Abstract : The use of public interfaces as a means of encapsulating method implementations has become standard in software design, but still requires the development of appropriate verification techniques. In this paper we study the consequences on verification of dividing methods into public and private ones. We introduce a notion of interface behaviour of applets which abstracts from the internal, private behaviour, and we propose an abstraction technique, based on inlining of private methods, to verify properties of this interface behaviour. We define the inlining transformation and prove that it preserves the properties expressible in our simulation logic. Our abstraction technique is particularly suitable for compositional verification, since it allows global system properties to be inferred from the interface properties of the components that are not yet available. In addition, we show on a concrete case study how the reduction in the number of methods resulting from the inlining transformation drastically improves the performance of the computationally most expensive step in the compositional verification technique previously developed by the authors.
Document type :
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 9:10:33 PM
Last modification on : Friday, February 4, 2022 - 3:17:28 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:41:21 PM


  • HAL Id : inria-00070670, version 1



Dilian Gurov, Marieke Huisman. Abstraction over Public Interfaces. [Research Report] RR-5330, INRIA. 2004, pp.21. ⟨inria-00070670⟩



Record views


Files downloads