Change search
ReferencesLink to record
Permanent link

Direct link
Interface abstraction for compositional verification
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2005 (English)In: SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings / [ed] Aichernig, BK; Beckert, B, 2005, 414-423 p.Conference paper (Refereed)
Abstract [en]

To support dynamic loading of applications on portable devices, one needs compositional reasoning techniques to ensure that newly loaded applications cannot break the overall security of a device. In earlier work, we developed an algorithmic verification technique for control flow based safety properties of smart card applications, which allows global system properties to be inferred from the properties of the components. Application of the technique requires knowledge of the names of all methods implemented by these components. In a truly compositional setting, however, one only knows the public interface of the new applet and does not have access to any implementation details. To compositionally verify interface properties of applets, one therefore has to combine our verification technique with an abstraction which preserves the interface behaviour and reduces the set of implemented methods to the set of public methods. In this paper we develop such an abstraction technique: we formally define the notion of interface behaviour and propose an inlining transformation which we prove to preserve the interface properties expressible in our specification language. In addition, we show on a concrete case study how the reduction in the number of methods resulting from the interface abstraction drastically improves the performance of the computationally most expensive step of the compositional verification technique.

Place, publisher, year, edition, pages
2005. 414-423 p.
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-43334ISI: 000232829700043ScopusID: 2-s2.0-46149103697ISBN: 0-7695-2435-4OAI: diva2:448405
3rd IEEE International Conference on Software Engineering and Formal Methods Location: Koblenz, Germany, Date: SEP 07-09, 2005
QC 20111017Available from: 2011-10-17 Created: 2011-10-14 Last updated: 2011-10-17Bibliographically approved

Open Access in DiVA

No full text


Search in DiVA

By author/editor
Gurov, DilianHuisman, Marieke
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 9 hits
ReferencesLink to record
Permanent link

Direct link