Abstract
Unmanned Aerial Vehicles (UAVs) have become useful tools in industries. In this paper, we verify the behavior of an autonomous UAV executing an inspection task. More specifically, we look into the use of the knowledge base system IDP as a verification tool. We propose an approach for the modeling and verification of the safety-critical UAV and its environment in IDP. The methodology and modeling choices that are beneficial for the performance of the verification task and the readability of the model are denoted. We identify the need for discrete domains and investigate the consequences. Verification is successfully achieved using both Bounded Model Checking (BMC) and Invariant Checking (IC).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
IDP stands for Imperative Declarative Programming. More information on IDP and its modeling language can be found here: https://dtai.cs.kuleuven.be/software/idp.
- 2.
A policy contains a mapping from every possible state of the system to the action that has to be executed in that state.
- 3.
The IDP model of the application at hand is available at https://github.com/VermaelenJan/Model-Checking-Drones-with-IDP/blob/master/model.idp.
- 4.
Non-determinism in IDP can be achieved by defining a predicate without initializing it. IDP will look for models regarding all possible values (of the relevant domain) for the predicate.
- 5.
The policy of the application at hand is available at https://github.com/VermaelenJan/Model-Checking-Drones-with-IDP/blob/master/Policy/Policy.pdf.
- 6.
For the policy of the application at hand, proof of completeness is provided at https://github.com/VermaelenJan/Model-Checking-Drones-with-IDP/blob/master/Policy/Completeness%20Policy/policy%20complete.pdf.
References
Alhawi, O.M., Mustafa, M.A., Cordeiro, L.C.: Finding security vulnerabilities in unmanned aerial vehicles using software verification. CoRR abs/1906.11488 (2019). http://arxiv.org/abs/1906.11488
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361), pp. 317–320, June 1999. https://doi.org/10.1109/DAC.1999.781333
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers, vol. 58, pp. 117–148. Elsevier (2003). https://doi.org/10.1016/S0065-2458(03)58003-2
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14
Bruynooghe, M., et al.: Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems with IDP3. Theory Pract. Logic Program. 15(6), 783–817 (2015). https://doi.org/10.1017/S147106841400009X
Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35746-6_1
Dinh, H.T., Cruz Torres, M.H., Holvoet, T.: Combining planning and model checking to get guarantees on the behavior of safety-critical UAV systems. In: ICAPS Workshop on Planning and Robotics (2018). https://lirias.kuleuven.be/retrieve/509824
Hoffmann, R., Ireland, M., Miller, A., Norman, G., Veres, S.: Autonomous agent behaviour modelled in PRISM – a case study. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 104–110. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-32582-8_7
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46029-2_13
Schumann, J., Visser, W.: Autonomy software: V & V challenges and characteristics. In: 2006 IEEE Aerospace Conference, pp. 1–6. IEEE (2006)
Sirigineedi, G., Tsourdos, A., White, B.A., Żbikowski, R.: Kripke modelling and verification of temporal specifications of a multiple UAV system. Ann. Math. Artif. Intell. 63(1), 31–52 (2011). https://doi.org/10.1007/s10472-011-9270-x
Torens, C., Adolf, F.M., Goormann, L.: Certification and software verification considerations for autonomous unmanned aircraft. J. Aerosp. Inf. Syst. 11(10), 649–664 (2014)
Acknowledgments
This research is partially funded by the Research Fund KU Leuven.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Vermaelen, J., Dinh, H.T., Holvoet, T. (2020). Formal Verification of Autonomous UAV Behavior for Inspection Tasks Using the Knowledge Base System IDP. In: Demazeau, Y., Holvoet, T., Corchado, J., Costantini, S. (eds) Advances in Practical Applications of Agents, Multi-Agent Systems, and Trustworthiness. The PAAMS Collection. PAAMS 2020. Lecture Notes in Computer Science(), vol 12092. Springer, Cham. https://doi.org/10.1007/978-3-030-49778-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-49778-1_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-49777-4
Online ISBN: 978-3-030-49778-1
eBook Packages: Computer ScienceComputer Science (R0)