Interface abstraction for compositional verification
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)
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.
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-43334ISI: 000232829700043ScopusID: 2-s2.0-46149103697ISBN: 0-7695-2435-4OAI: oai:DiVA.org:kth-43334DiVA: diva2:448405
3rd IEEE International Conference on Software Engineering and Formal Methods Location: Koblenz, Germany, Date: SEP 07-09, 2005
QC 201110172011-10-172011-10-142011-10-17Bibliographically approved