Safe resource-aware virtual machines for IoT devices

Funder

Organizational Unit

Publications

Safe and resource-aware verification for programming Cyber-Physical Systems

Publication . Mão De Ferro, Carlos; Martins, Francisco Cipriano da Cunha; Costa, António Casimiro Ferreira da

Cyber-physical systems (CPS) integrate computation with physical processes and are expected to influence nearly 30 billion devices globally by 2030. Developing software for these systems presents unique challenges, especially in critical and resource-constrained scenarios. A predominant issue is the integration of multiple stateful systems, where the incorrect sequence of function calls compromises the overall system functionality. Formal verification increases safety, but its application is often confined to experts. This thesis presents Shelley, a novel model checking framework that streamlines the verification of function call order when integrating stateful systems. Shelley uniquely allows developers to specify temporal requirements closely aligned with the source code and automates the verification process. The framework’s ability to generate behavior diagrams and show intuitive counterexamples further assists developers in analyzing the program behavior, ensuring that the software is safe and adheres to its specified requirements. An evaluation is provided, which includes rigorous case studies such as NASA’s PHALANX experiment and an industrial setting, demonstrating the framework’s broad applicability and effectiveness in identifying invalid behaviors. Our contributions through the Shelley framework include the formalization of the process of extracting models from MicroPython code, as well as a new specification language tailored for verifying call order. In addition, we establish the decidability of checking system usage via automata theory and we introduce an automated process for checking requirements that utilizes temporal logic over finite traces. Together, these advancements simplify the incorporation of formal verification into high-level programming contexts, ensuring that more programmers can deliver safer software.

2025-02-06Doctoral thesis

Open access