Improving the Reliability of Mobility Applications

TL;DR

This paper demonstrates how Event-B, a formal method, can be used to verify and document the design of Android applications, exemplified through a case study on WhatsApp's core functionalities.

Contribution

It shows the practical application of heavyweight Formal Methods with Event-B for ensuring correctness in Android app development, including modeling and verification.

Findings

Event-B effectively supports Android app correctness verification.

Modeling core functionalities aids in documenting design decisions.

Case study on WhatsApp illustrates practical application.

Abstract

The Android platform was introduced by Google in 2008 as an operating system for mobile devices. Android's SDK provides a wide support for programming and extensive examples and documentation. Reliability is an increasing concern for Smart Phone applications since they often feature personal information and data. Therefore, techniques and tools for checking the correct behavior of apps are required. This paper shows how the Event-B method can be used to reason and to verify the design of Android apps and how this can be used to document implementation decisions. Our approach consists in modeling the core functionality of the app in Event-B and using the evidence shown by the Proof Obligations generated to reason about the design and the implementation of the app. Although we do not propose a novel approach, we prove that heavyweight Formal Methods (FMs) techniques with Event-B can effectively be used to support the development of correct Android apps. We present a case study in which we design the core functionality of WhatsApp in Event-B, we encode it over three machine refinements modeling basic functionality (chatting, deleting content, forwarding content, deleting a chat session, etc.), read and unread status of chat sessions, and implementation details, respectively. We report and discuss on underlying challenges in the design and implementation of the core functionality.