Applications running on mobile devices are subject to frequent changes in connectivity to back-end infrastructure. In order not to disrupt service and ensure fault-tolerant operation, transaction-oriented mobile applications must be able to operate in both online and offline mode. Recently, a generic software architecture has been proposed [4] to accommodate mobile transaction models that support offline transaction processing in conjunction with data replication, reintegration, and synchronisation. We present an initial Coloured Petri Net (CPN)[2] model of a mobile transaction system and report on the first results on verifying its behavioural correctness using model checking.

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.