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

IET Cyber-Physical Systems

¹  Iury V. Bessa²  Lucas C. Cordeiro³  Eddie B. de Lima Filho⁴ 

[1] ;Federal University of Amazonas;School of Computer Science, University of Manchester;TPV Technology;

关键词: formal verification;    software architecture;    multiprocessing systems;    embedded systems;    cyber-physical systems;    system class;    ecps;    system development;    test vectors;    assertion-based verification;    high-level processor models;    meeting time;    energy constraints;    concurrent software;    operation logic;    symbolic model checking techniques;    reliability issues;    correct-by-construction systems;    automated symbolic verification;    embedded systems;    automotive device control;    health care;    mobile devices;    internet of things;    consumer electronics;    multicore processors;    signal-processing pipelines;    computational power;    cyber-physical systems;   

DOI  :  10.1049/iet-cps.2018.5006

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown