Special talk by Sergio Mover on Abstractions and models to design safe Event-Driven Cyber-Physical Systems

Abstract: In a cyber-physical system digital computations (e.g., a hardware component or a program) interact with the physical environment. We find examples of such systems in different domains like aerospace, automotive, and medical devices where a failure in the design of the system may have serious consequences. More recently, Cyber-Physical Systems are integrating the use of mobile devices, like Android phones, due to their hardware, their rich Application Programming Interface (API), and their event-driven programming model that allows them to react to the user interaction or the physical environment. This new adoption complicates the verification of Cyber-Physical systems, due to the complexity of the software, and the lack of formal design techniques, for mobile devices. In this talk, I will first describe my work on formal verification for cyber-physical systems based on relational abstraction, where we reduce the verification problem of a hybrid (continuous and discrete) system to the verification of a purely discrete system.

Then, I will focus on a key problem that arises when developing Android programs, the protocol violation problem. The developer of an Android application writes code (e.g., the Android application) that is invoked by the framework (e.g., Android) when receiving an external event. The main effect of this model is that the order of execution of the application code is determined both by the non-deterministic events and by the internal implementation of the framework. In these settings, a developer must not violate the protocol imposed by the framework to avoid unexpected behaviors. The main challenge is that the protocol is implicit in the framework implementation. I will show how we can precisely formalize the framework's protocol, learn it automatically using active learning techniques, and develop an algorithm that verifies the existence of protocol violations.

I will conclude the talk presenting the future research challenges in the implementation and verification of event-driven Cyber-Physical systems.