Better Late Than Never: Verification of Embedded Systems After Deployment

Martin Ring, Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler

In: Design, Automation & Test in Europe. Design, Automation & Test in Europe (DATE-2019) March 25-29 Florence Italy 2019.


This paper investigates the benefits of verifying embedded systems after deployment. We argue that the huge state spaces of contemporary embedded and cyber-physical systems are caused by the large variety of operating contexts, which are unknown during development. Once the system is deployed, these contexts become observable, confining several variables. By this, the search space is dramatically reduced, making verification possible even on the limited resources of a deployed system. In this paper, we propose a design and verification flow which exploits this observation. We show how specifications are transferred to the deployed system and verified there. Evaluations on a number of case studies demonstrate the reduction of the search space, and we sketch how the proposed approach can be employed in practice.


date2019_-_better_late_than_never_verification_of_embedded_systems_after_deployment.pdf (pdf, 277 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence