Publication
Let's Prove It Later --- Verification at Different Points in Time
Martin Ring; Christoph Lüth
In: Peter Csaba Ölveczky; Gwen Salaün (Hrsg.). Software Engineering and Formal Methods - 17th International Conference, Proceedings. International Conference on Software Engineering and Formal Methods (SEFM-2019), September 16-20, Oslo, Norway, Pages 454-468, Lecture Notes in Computer Science (LNCS), Vol. 11724, ISBN 978-3-030-30446-1, Springer, Cham, 9/2019.
Abstract
The vast majority of cyber-physical and embedded systems today is deployed without being fully formally verified during their design. Postponing verification until after deployment is a possible way to cope with this, as the verification process can benefit from instantiating operating parameters which were unknown at design time. But there exist many interesting alternatives between early verification (at design time) and late verification (at runtime). Moreover, this decision also has an impact on the specification style. Using a case study of the safety properties of an access control system, this paper explores the implications of different points in time chosen for verification, and points out the respective benefits and trade-offs. Further, we sketch some general rules to govern the decision when to verify a system.