Formal Verification of Autonomous System Software
Sunil Anasuri · International Journal of Emerging Research in Engineering and Technology · 2022
Autonomous systems are transforming numerous industries such as the automotive industry, aerospace industry, robotics and defence industries. Such systems are taking on increasingly safety-critical roles, and thus, reliability and correctness are critical components. Formal verification provides mathematically sound methods of establishing or proving the falseness of software relative to a given formal specification or property. In this paper, a thorough analysis of the formal verification of autonomous system software is offered, including the theoretical background, practical applications, tools and instances of application in a number of fields. Model checking, theorem proving, and Runtime verification are highlighted as the main formal methods. In the course of the critical review of the state-of-the-art, we provide evidence of the achievements and shortcomings of formal verification methods, especially under real-time, adaptive, and AI-controlled autonomous systems. This paper talks of incorporating formal verification in the software development process, its contribution to certification of safety, and its relationship with simulation and testing. The findings reveal the sources of contributions of formal methods in error-early detection, better assurances of safety and a greater 게 increase in robustness of the systems. Conclusively, we state the view that the future challenges will be issues of scalability, the verification of the elements of machine learning, and the development of more user-friendly toolchains to increase industry adoption