Event-driven programming is widely used in mobile (e.g. Android and iOS) and embedded (e.g. TinyOS) systems, since the application code must respond to events generated by the external environment (e.g. the user clicks the screen of the phone, a new data is read is received from a network connection...).
A developer programs an event-driven application by implementing its code in event handlers methods, called callbacks, invoking the application-programming interface (API) methods provided by the system's framework, called callins, while the framework invokes callback methods when events happen.
In order to develop reliable event-driven applications, the developer must not violate the application-programming protocol imposed by the framework. A violation happens when the application code invokes an API method, but the underlying framework is in a state that prohibits it, resulting in an unexpected behaviors (e.g. the application crashes).
Reasoning about protocol violations is notoriously difficulty for a developer, since the possible execution of callbacks and callins is determined by the whole sequence of callbacks and callins previously executed by application, which in turn determines the internal state of the framework.
In this talk we will focus on an approach that enables to reasons about protocol violations in event-driven applications.
We first identify the key aspects of an event-driven framework that are relevant to capture the application-programming protocol, and we formalize a core abstract machine model that captures them. Based on this formalization, we introduce a specification language (lifestate specification) that is adequate to describe the protocol. We present a dynamic verification technique that, given a specification of the protocol and an existing, non-crashing, trace of execution, can either predict the existence of protocol violations or prove their absence.
We instantiate the approach for the Android framework, and we show an experimental evaluation on real Android applications.