Formal Verification of Autonomous System Software
DOI:
https://doi.org/10.63282/3050-922X.IJERET-V3I1P110Keywords:
Formal verification, autonomous systems, model checking, theorem proving, runtime verificationAbstract
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
References
[1] Lamport, L. (1977). Proving the correctness of multiprocess programs. IEEE transactions on software engineering, (2), 125-143.
[2] Cousot, P., & Cousot, R. (1977, January). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (pp. 238-252).
[3] Havelund, K., & Roşu, G. (2004). An overview of the runtime verification tool Java PathExplorer. Formal methods in system design, 24, 189-215.
[4] Barrett, C., & Tinelli, C. (2018). Satisfiability modulo theories. Handbook of model checking, 305-343.
[5] Bengtsson, J., & Yi, W. (2003, September). Timed automata: Semantics, algorithms and tools. In Advanced Course on Petri Nets (pp. 87-124). Berlin, Heidelberg: Springer Berlin Heidelberg.
[6] Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., ... & Winwood, S. (2009, October). seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (pp. 207-220).
[7] André, É., Fribourg, L., Kühne, U., & Soulat, R. (2012, August). IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In International Symposium on Formal Methods (pp. 33-36). Berlin, Heidelberg: Springer Berlin Heidelberg.
[8] Rizaldi, A., & Althoff, M. (2015, September). Formalising traffic rules for the accountability of autonomous vehicles. In 2015 IEEE 18th International Conference on Intelligent Transportation Systems (pp. 1658-1665). IEEE.
[9] Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical computer science, 126(2), 183-235.
[10] Dreossi, T., Donzé, A., & Seshia, S. A. (2019). Compositional falsification of cyber-physical systems with machine learning components. Journal of Automated Reasoning, 63(4), 1031-1053.
[11] Ingrand, F. (2019, February). Recent trends in formal validation and verification of autonomous robots' software. In 2019, Third IEEE International Conference on Robotic Computing (IRC) (pp. 321-328). IEEE.
[12] Cardoso, R. C., Kourtis, G., Dennis, L. A., Dixon, C., Farrell, M., Fisher, M., & Webster, M. (2021). A review of verification and validation for space autonomous systems. Current Robotics Reports, 2(3), 273-283.
[13] Sun, X., Khedr, H., & Shoukry, Y. (2019, April). Formal verification of neural network-controlled autonomous systems. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (pp. 147-156).
[14] Luckcuck, M., Farrell, M., Dennis, L. A., Dixon, C., & Fisher, M. (2019). Formal specification and verification of autonomous robotic systems: A survey. ACM Computing Surveys (CSUR), 52(5), 1-41.
[15] Dennis, L., Fisher, M., Slavkovik, M., & Webster, M. (2016). Formal verification of ethical choices in autonomous systems. Robotics and Autonomous Systems, 77, 1-14.
[16] Fisher, M., Mascardi, V., Rozier, K. Y., Schlingloff, B. H., Winikoff, M., & Yorke-Smith, N. (2021). Towards a framework for certification of reliable autonomous systems. Autonomous Agents and Multi-Agent Systems, 35, 1-65.
[17] Zaki, O., Dunnigan, M., Robu, V., & Flynn, D. (2021). Reliability and safety of autonomous systems based on semantic modelling for self-certification. Robotics, 10(1), 10.
[18] Goncalves, F. S., Pereira, D., Tovar, E., & Becker, L. B. (2017, November). Formal verification of AADL models using UPPAAL. In 2017 VII Brazilian Symposium on Computing Systems Engineering (SBESC) (pp. 117-124). IEEE.
[19] Zha, H., van der Aalst, W. M., Wang, J., Wen, L., & Sun, J. (2011). Verifying workflow processes: a transformation-based approach. Software & Systems Modeling, 10, 253-264.
[20] Antsaklis, P. J., Stiver, J. A., & Lemmon, M. (1991, June). Hybrid system modeling and autonomous control systems. In International Hybrid Systems Workshop (pp. 366-392). Berlin, Heidelberg: Springer Berlin Heidelberg.
[21] Pappula, K. K. (2020). Browser-Based Parametric Modeling: Bridging Web Technologies with CAD Kernels. International Journal of Emerging Trends in Computer Science and Information Technology, 1(3), 56-67. https://doi.org/10.63282/3050-9246.IJETCSIT-V1I3P107
[22] Rahul, N. (2020). Optimizing Claims Reserves and Payments with AI: Predictive Models for Financial Accuracy. International Journal of Emerging Trends in Computer Science and Information Technology, 1(3), 46-55. https://doi.org/10.63282/3050-9246.IJETCSIT-V1I3P106
[23] Enjam, G. R. (2020). Ransomware Resilience and Recovery Planning for Insurance Infrastructure. International Journal of AI, BigData, Computational and Management Studies, 1(4), 29-37. https://doi.org/10.63282/3050-9416.IJAIBDCMS-V1I4P104
[24] Pappula, K. K., & Rusum, G. P. (2021). Designing Developer-Centric Internal APIs for Rapid Full-Stack Development. International Journal of AI, BigData, Computational and Management Studies, 2(4), 80-88. https://doi.org/10.63282/3050-9416.IJAIBDCMS-V2I4P108
[25] Pedda Muntala, P. S. R. (2021). Integrating AI with Oracle Fusion ERP for Autonomous Financial Close. International Journal of AI, BigData, Computational and Management Studies, 2(2), 76-86. https://doi.org/10.63282/3050-9416.IJAIBDCMS-V2I2P109
[26] Rahul, N. (2021). AI-Enhanced API Integrations: Advancing Guidewire Ecosystems with Real-Time Data. International Journal of Emerging Research in Engineering and Technology, 2(1), 57-66. https://doi.org/10.63282/3050-922X.IJERET-V2I1P107
[27] Enjam, G. R., & Chandragowda, S. C. (2021). RESTful API Design for Modular Insurance Platforms. International Journal of Emerging Research in Engineering and Technology, 2(3), 71-78. https://doi.org/10.63282/3050-922X.IJERET-V2I3P108
