Self-Verification - Verification of Embedded Systems after Deployment

Abstract

This thesis introduces self-verification, an approach to verifying embedded systems that complements traditional a priori verification by postponing parts of the proofs until after the system is deployed. By leveraging the concrete values of parameters that become known at run-time, self-verification aims to alleviate the state space explosion problem, a significant challenge in verification. The fundamentals of self-verification are explored through case studies and a tool chain supporting specification in SysML/OCL, system modeling in Clash, and run-time verification using SMT provers and SAT solvers. The impact of self-verification on the development process is investigated, providing guidelines for its application and a methodology to identify variables that can potentially reduce verification time when instantiated at run-time. The thesis discusses the potential of self-verification to improve the safety, reliability, and efficiency of embedded systems, while acknowledging the challenges that need to be addressed to fully realise its benefits. This work contributes to the ongoing research in verification techniques and lays the groundwork for further exploration of self-verification and its integration into the design process.