A complete assertion-based verification framework from the edge to the cloud

Assertion-based verification (ABV) is a well-known approach for checking the functional correctness of a system. Since modern cyber-physical systems are increasingly complex and distributed, it is no longer appropriate applying ABV only to the single components; instead, it is necessary to embrace holistic approaches that look at the entire system. Furthermore, due to the dynamic nature of the system under verification (SUV), ABV cannot be applied only in an offline fashion. Alternatively, it is necessary to extend the verification process to the post-deployment phase; however, this collides with the issues of dealing with a distributed system affected by unpredictable latency and providing limited computational resources. Therefore, it becomes essential to develop a dynamic orchestration approach where checkers perform runtime verification without negatively influencing the computation of the functional parts of the SUV. To fill in the gap, I propose a complete framework to verify complex distributed systems, from the formalisation of specifications to runtime execution. The proposed framework aims at covering several holes in the verification process of systems executing in an edge-to-cloud computing environment.