Survey on automated symbolic verification and its application for synthesising cyber-physical systems

Abstract

Dependency on the correct operation of embedded systems is rapidly growing, mainly due to their wide range of applications. Their structures are becoming more complex and currently require multi-core processors with scalable shared memory, signal-processing pipelines, and sophisticated software modules to meet increasing computational power, flexibility demands. Additionally, interaction with real-world entities and modern communication capabilities further enhance the mentioned features and give rise to the embedded and cyber-physical systems (ECPS). As a consequence, the reliability of ECPS becomes a key issue during system development. Generally, state-of-the-art verification methodologies for ECPS generate test vectors and use assertion-based verification and high-level processor models, during simulation; however, new challenges arose, such as need for meeting time and energy constraints, handling concurrent software, evaluating implementation-structure choices, ensuring correct system behavior together with physical plants, and supporting new software architectures and legacy designs. This survey deals with the mentioned issues, reviews related literature, and discusses recent advances in symbolic model checking techniques and their applications to control synthesis. Additionally, challenges, problems, and recent advances to ensure correctness and timeliness, regarding ECPS, are discussed. Reliability issues, when developing ECPS, are then considered, as a prominent verification and synthesis application for achieving correct-by-construction systems.