Home → News and Events → Colloquia → Colloquium
When: 10:00AM - 11:30AM , March 06, 2018
Speaker: Dr. Sergio Mover
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.
Mobile devices, like Android phones, are increasingly used in Cyber-Physical Systems, 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.
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 the protocol violation problem that arises when developing Android programs. 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.
Dr. Sergio Mover is a postdoctoral researcher in the Computer Science Department at the University of Colorado Boulder. His main research focuses on the development of theory and tools to formally verify Cyber-Physical systems, embedded software, and Android apps, and in applying machine learning and data mining techniques to learn software properties from existing code bases. Sergio received his Ph.D. degree from the University of Trento and Fondazione Bruno Kessler, Italy, where he worked on formal verification algorithms for hybrid systems and embedded software using Satisfiability Modulo Theories