Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070670
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 9:10:33 PM
Last modification on : Saturday, January 27, 2018 - 1:31:03 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:41:21 PM

Identifiers

  • HAL Id : inria-00070670, version 1

Collections

Citation

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

Share

Metrics

Record views

103

Files downloads

63