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
Checking absence of illicit applet interactions: A case study
2004 (English)In: FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS / [ed] Wermelinger, M; MargariaSteffen, T, BERLIN: SPRINGER , 2004, Vol. 2984, 84-98 p.Conference paper, Published paper (Refereed)
Abstract [en]

This paper presents the use of a method - and its corresponding tool set - for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.

Place, publisher, year, edition, pages
BERLIN: SPRINGER , 2004. Vol. 2984, 84-98 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 2984
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-43984ISI: 000189499800006Scopus ID: 2-s2.0-35048820515ISBN: 3-540-21305-8 (print)OAI: oai:DiVA.org:kth-43984DiVA: diva2:450874
Conference
7th International Conference on Fundamental Approaches to Software Engineering. Barcelona, SPAIN. MAR 29-APR 02, 2004
Note
QC 20111024Available from: 2011-10-24 Created: 2011-10-19 Last updated: 2011-10-24Bibliographically approved

Open Access in DiVA

No full text

Scopus

Authority records BETA

Gurov, Dilian

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
KTH
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 27 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