RV'21

Title: Bringing Runtime Verification to the Masses

Abstract

Real-world behavior of systems can deviate excessively from the behavior shown under certification conditions. 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). The RDE regulations come with an informal but relatively precise specification that spells out in how far a real trip, i.e., a trajectory driven with a car in-the-wild, constitutes an RDE test, or not. This presentation starts off with discussing a formalization of the RDE specification in RTLola, a real-time extension of the stream-based specification language Lola. It then presents 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. Joint work with Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian A. Köhl, Yannik Schnitzer, and Maximilian Schwenger

Bio

Holger Hermanns is full professor at Saarland University, Saarbrücken, Germany, holding the chair of Dependable Systems and Software on Saarland Informatics Campus. He has previously held positions at Universität Erlangen-Nürnberg, Germany, at Universiteit Twente, the Netherlands, and at INRIA Grenoble Rhône-Alpes, France, and is former Dean of the Faculty of Mathematics and Computer Science at Saarland University. His research interests include modeling and verification of concurrent systems, resource-aware embedded systems, compositional performance and dependability evaluation, and their applications to energy informatics. He is an outspoken proponent of proactive algorithmic accountability. Holger Hermanns has authored or co-authored more than 200 peer-reviewed scientific papers (ha-index 92, h-index 48). He co-chaired the program committees of major international conferences such as CAV, CONCUR, TACAS and QEST, and delivered keynotes at about a dozen international conferences and symposia. He serves on the steering committees of ETAPS and TACAS. He is president of the association "Friends of Dagstuhl e.V.", and vice president of the association "ETAPS e.V.". Holger Hermanns received the Dutch "Vernieuwingsimpuls" and the German "Preis des Fakultätentages Informatik" award. He is an ERC Advanced Grantee and elected member of Academia Europaea, and holds several other national and European research grants.