In this seminar I plan to survey two research endeavours we are actively pursuing as part of a larger initiative on perspicuous computing.
First, I will discuss the application of formal modelling, verification and optimisation methods in Low-Earth Orbit (LEO). The operation of LEO small satellites rests on a fine balance between solar power in feed and power demands of observation and communication technologies on board, buffered by on-board battery storage. We address the resulting control problem by a sophisticated combination of dynamic programming and learning techniques based on profound battery and electric power budget models. These models are continually kept accurate by extrapolating data from telemetry received from satellites. The resulting software infrastructure delivers optimal, efficient, scalable, usable, and robust operation plans, which are provisioned to the satellites without need for human intervention. The approach has been validated in orbit on the dual-satellite mission GOMX–4 by GOMSPACE. It is currently being matured into a commercial software product, made possible by a dedicated grant from the ERC.
Second, I will turn to the use of formal modelling and runtime verification for the purpose of diagnosing the exhaust emissions of cars in-the-wild. In response to the massive revelation of fraudulent behavior programmed inside diesel cars across Europe, the European Union has defined a procedure to test for Real Driving Emissions (RDE) on public roads. We discuss a formalization of the RDE specification in RTLola, a real-time extension of the stream-based specification language Lola. Then I present the crucial technology enabling everyday car owners to monitor the behaviour of their cars. Concretely, we have developed an Android app that deploys RTLola runtime monitors on smart phones for the purpose of diagnosing automotive exhaust emissions during RDE tests. For this, we harvest the availability of cheap bluetooth adapters to the On-Board-Diagnostics (OBD) ports, which are ubiquitous in cars nowadays. As such, the LolaDrives app makes runtime verification accessible to millions of car owners for the purpose of checking RDE specification conformance of their cars. We discuss lessons learnt and ongoing developments.
Join at http://imt.lu/seminar