Formal reasoning about non-atomic JAVA CARD methods in Dynamic Logic

Abstract

We present an extension to JAVA CARD Dynamic Logic, a program logic for reasoning about JAVA CARD programs, to handle JAVA CARD'S so-called non-atomic methods. Although JAVA CARD DL already supports the atomic transaction mechanism of JAVA CARD, non-atomic methods present an additional challenge: state updates triggered by such a non-atomic method are not subjected to any transaction that may possibly be in progress. The semantics of a non-atomic method itself seems to be simple and straightforward to formalise, however experimental studies showed that non-atomic methods affect the whole semantics of the JAVA CARD transaction mechanism in a subtle way, in particular, it affects the notion of a transaction roll-back. In this paper we show how to adapt JAVA CARD DL to accommodate this newly discovered complex transaction behaviour. The extension completes the formalisation of all of JAVA CARD in Dynamic Logic. © Springer-Verlag Berlin Heidelberg 2006.