A formal approach for identifying assurance deficits in unmanned aerial vehicle software
Abstract
While formal methods have proved to be unfeasible for large scale systems, argument-based safety cases offer a plausible alternative basis for certification of critical software. Our proposed method for increasing safety combines formal methods with argumentation-based reasoning. In a first step, we provide a formal representation of the the argumentative-based Goal Structuring Notation (GSN) standard used in industry. In a second step, our solution exploits reasoning in description logic to identify assurance deficits in the GSN model. The identified flaws are given to a hybrid logic-based model checker to be validated against a Kripke model. The method is illustrated for an unmanned aerial vehicle software, with reasoning performed in RacerPro engine and the HLMC model checker based on hybrid logic.
Full citation
"A formal approach for identifying assurance deficits in unmanned aerial vehicle software", A. Groza, I. A. Letia, A. Goron and S. Zaporojan, In Proceedings of 23 International Conference on Systems Engineering (Advances in Intelligent Systems \& Computing Series), Las Vegas, USA Springer International Publishing, Vol. 1089, pp. 233-239, DOI: 10.1007/978-3-319-08422-0_35, ISBN: 978-3-319-08422-0, 2015.