Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published 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 Sciences
Identifiers
URN: urn:nbn:se:kth:diva-43334ISI: 000232829700043Scopus ID: 2-s2.0-46149103697ISBN: 0-7695-2435-4 (print)OAI: oai:DiVA.org:kth-43334DiVA: diva2:448405
Conference
3rd IEEE International Conference on Software Engineering and Formal Methods Location: Koblenz, Germany, Date: SEP 07-09, 2005
Note
QC 20111017Available from: 2011-10-17 Created: 2011-10-14 Last updated: 2018-01-12Bibliographically approved

Open Access in DiVA

No full text

Scopus

Authority records BETA

Gurov, Dilian

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 17 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf