  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.
