Formal Veriftcation of Aircraft, Uboat and Electric Car Control Systems using SPARK ADA

Abstract

The control systems of safety-critical transportation vehicles such as railways, submarines, and electric carsmust bedesignedandver ifiedri gorously to ensure their safe and reliable operation. In this paper, we present a formal verification approach using the SPARK ADA programming language toverify the correctness of control systems for these vehicles. SPARK ADA isalanguage that enforces strong static typing, and provides formal verification support through contracts and proof obligations. We demonstrate the effectiveness of our approach by applying it to three case studies: a railway control system, a submarine control system, and an electric car control system. For each case study, we first specify the system requirements and design the control system using SPARK ADA. We then perform formal verification by generating and proving proof obligations using the SPARK toolset.
Our resultsshow that our approach is effective in detecting and preventing potential errors and vulnerabilities in the control systems. In particular, we found several subtle errors in the case studies that were not detected by traditional testing or manual inspection. Furthermore, our approachenables us to prove that the control systems satisfy their specified requirements, which is crucial for ensuring their safety and reliability.
In conclusion, our approach using SPARK ADA provides a rigorous and efficient method for formal verification of control systems for safety-critical transportation vehicles. It can help designers and engineers to ensure the correctness and reliability of their control systems, and reduce the risk of accidents and incidents.