Introduction. Mobile client applications often need to execute transactions that read and write shared data sets stored on a server-side infrastructure. Examples include applications involving local payment, where concurrently running applications need access to funds from a shared account. A challenge in this scenario is that mobile devices may often loose connectivity. To avoid disruption of service, the application must be able to operate even when the mobile device is offline. This requires specialised transaction models that replicate data for offline operation and which synchronise data when coming back online.

Several conflict-free transaction models have been proposed to support such scenarios. As an example, the Escrow transaction model [3] is based on a logical split of the shared data set, and can be used to for instance give a mobile application access to a restricted amount of funds on an account. Vaupel et al. [4] have proposed a generic architecture that includes online and offline transaction processing, replication, synchronisation and re-integration of data and which is able accommodate different conflict-free mobile transaction models.

CPN model. Our goal is to develop a formal executable specification of the mobile transaction architecture proposed in [4]. In particular, we want to verify the correctness of conflict-free transactions for a given mobile application. Furthermore, the CPN model should reflect the architecture and make it easy to change the set of transactions for a concrete mobile application.

Figure 1 shows the CPN module of the local transaction manager on the mobile client for an example with a Debit transaction operating on a shared Amount. The application invokes the debit transaction via the Application place. When operating in offline mode, the transactions executed are written in a Log. The substitution transitions Synchronise and Replicate represent the two major operational modes that allow data to be synchronised with the server-side when online, and conflict-free replication of data to support offline operation. The places CtoS and StoC are used for modelling the communication between the client-side and the server-side.

Verification. We perform verification using explicit-state model checking, as supported by CPN Tools [1]. The state space for the Escrow-based payment transaction system with a debit transaction has 7, 174 states and 22, 202 edges and can be generated in less than three seconds. The transaction model replicates the amount on the account such that all mobile clients have access to an equal amount. A key property of the application is that independently of how the clients go online and offline, it should always be possible to return to a consistent state in which the sum of the amounts replicated to the clients is equal to the total amount stored on the server-side. In computation tree logic (CTL), this property can be expressed as AG EF p, where p is a state predicate expressing that the state is consistent with respect to the amount.