Better Late Than Never Verification of Embedded Systems After Deployment
Martin Ring1, Fritjof Bornebusch1, Christoph Lüth1,2, Robert Wille1,3 and Rolf Drechsler1,2
1Cyber-Physical Systems, DFKI GmbH, Bremen, Germany
2Mathematics and Computer Science, University of Bremen, Germany
3Institute for Integrated Circuits, Johannes Kepler University Linz, Austria
ABSTRACT
This paper investigates the benefits of verifying embedded systems after deployment. We argue that one reason for the huge state spaces of contemporary embedded and cyberphysical systems is the large variety of operating contexts, which are unknown during design. 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.
