Mark, a Reasoning Kit for Mobility

The experience gained to date in the development of network applications has shown the difficulties of using traditional software technologies: reasoning about network applications is subtly different from reasoning about ordinary programs because of stronger requirements on security, different forms of termination, and phenomena like mobility and network-awareness. There are currently no standard methods, techniques and tools to support specification, development and (property) certification of these applications.To support property certification of network applications, we propose to use the network-aware logic Mobadtl and its proof assistant, Mark (Mobadtl Reasoning Kit). In the paper we present the prototype implementation of Mark and, as a validating example, we consider applications where mobile components are allowed to carry some resources with them when moving around the network.