Skip to main content
SpringerLink
Log in

Model Checking for Verification in UAV Cooperative Control Applications

  • Chapter
Book cover Recent Advances in Research on Unmanned Aerial Vehicles

Part of the book series: Lecture Notes in Control and Information Sciences ((LNCIS,volume 444))

Abstract

Recently, there has been an increased interest in verification techniques for complex, autonomous systems. Consider for instance a scenario in which individual autonomous agents must work together to complete a series of constrained tasks. In cases such as this, there is a need for techniques to verify that the agents interact correctly, i.e. that they are able to cooperatively complete the required tasks while satisfying the constraints. Current research suggests that standard software modeling and verification techniques such as model checking can be extended to meet this need. Here, we explore the use of model checking for verification in three scenarios that include a team of unmanned aerial vehicles. The first scenario involves a centralized cooperative control scheme, the second involves a decentralized cooperative control scheme, and the third involves high-levelmission planning. For these scenarios, tasks and constraints are written in linear temporal logic, scenario models are coded in Promela, and the models are verified using the model checker Spin.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  2. Baier, C., Joost-Pieter, K.: Principles of Model Checking. The MIT Press (2008)

    Google Scholar 

  3. Boehm, B.: Software and Its Impact: A Quantitative Assessment. Rand Corp. (1972)

    Google Scholar 

  4. Boehm, B.: Software engineering economics. IEEE Transactions on Software Engineering SE-10(1), 4–21 (1984)

    Article  Google Scholar 

  5. Boehm, B.: A view of 20th and 21st century software engineering. In: Proceedings of the 28th International Conference on Software Engineering, pp. 12–29. ACM (2006)

    Google Scholar 

  6. Campos, J.C., Harrison, M.D.: Formally verifying interactive systems: A review. In: Proceedings of the Fourth International Eurographics Workshop on Design, Specification, and Verification of Interactive Systems, pp. 109–124 (1997)

    Google Scholar 

  7. Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 33–51. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM) 50(5), 752–794 (2003)

    Article  MathSciNet  Google Scholar 

  9. Dahm, W.: Report on technology horizons: A vision for Air Force science & technology during 2010-2030. Technical report, United States Air Force (2010)

    Google Scholar 

  10. Edwards, S., Lavagno, L., Lee, E.A., Sangiovanni-Vincentelli, A.: Design of embedded systems: Formal models, validation, and synthesis. Proceedings of the IEEE 85(3), 366–390 (1997)

    Article  Google Scholar 

  11. Fisher, J., Henzinger, T.A.: Executable cell biology. Nature Biotechnology 25(11), 1239–1249 (2007)

    Article  Google Scholar 

  12. Fisher, M., Bordini, R.H., Hirsch, B., Torroni, P.: Computational logics and agents: A roadmap of current technologies and future trends. Computational Intelligence 23(1), 61–91 (2007)

    Article  MathSciNet  Google Scholar 

  13. Gerth, R.: Concise promela reference (1997), http://spinroot.com/spin/Man/Quick.html (accessed April 2011)

  14. Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278–292. IEEE (1996)

    Google Scholar 

  15. Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer (STTT) 1(1), 110–122 (1997)

    Article  MATH  Google Scholar 

  16. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  17. Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–294 (1997)

    Article  MathSciNet  Google Scholar 

  18. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley Publishing Company (2004)

    Google Scholar 

  19. Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proceedings of the FORTE 1994 Conference (1994)

    Google Scholar 

  20. Horowitz, R., Varaiya, P.: Control design of an automated highway system. Proceedings of the IEEE 88(7), 913–925 (2000)

    Article  Google Scholar 

  21. Iglesias, C.A., Garijo, M., González, J.C.: A survey of agent-oriented methodologies. In: Papadimitriou, C., Singh, M.P., Müller, J.P. (eds.) ATAL 1998. LNCS (LNAI), vol. 1555, pp. 317–330. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  22. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS (LNBI), vol. 5688, pp. 218–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Jiang, Z., Pajic, M., Connolly, A., Dixit, S., Mangharam, R.: Real-time heart model for implantable cardiac device validation and verification. In: 22nd Euromicro Conference on Real-Time Systems (ECRTS 2010), pp. 239–248. IEEE (2010)

    Google Scholar 

  24. Karaman, S., Frazzoli, E.: Vehicle routing with linear temporal logic specifications: Applications to multi-UAV mission planning. In: Proceedings of the AIAA Conference on Guidance, Navigation, and Control (2008)

    Google Scholar 

  25. Kent, S.: Model driven engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286–298. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Kumar, R., Krogh, B.H.: Heterogeneous verification of embedded control cystems. In: Proceedings of the IEEE American Control Conference, ACC 2006 (2006)

    Google Scholar 

  27. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 2.0: A tool for probabilistic model checking. In: Proceedings of the First International Conferece on Quantitative Evaluation of Systems (QEST 2004), pp. 322–323. IEEE (2004)

    Google Scholar 

  28. Lee, I., Pappas, G.J., Cleaveland, R., Hatcliff, J., Krogh, B.H., Lee, P., Rubin, H., Sha, L.: High-confidence medical device software and systems. IEEE Computer 39(4), 33–38 (2006)

    Article  Google Scholar 

  29. Long, D.E.: Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie Mellon University (1993)

    Google Scholar 

  30. Lygeros, J., Godbole, D.N., Sastry, S.: Verified hybrid controllers for automated vehicles. IEEE Transactions on Automatic Control 43(4), 522–539 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  31. Pneuli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science (FOCS 1977), pp. 46–67. IEEE Computer Society Press (1977)

    Google Scholar 

  32. Rajan, S., Shankar, N., Srivas, M.K.: An integration of model checking with automated proof checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 84–97. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  33. Royce, W.W.: Managing the development of large software systems. In: Proceedings of IEEE WESCON (1970)

    Google Scholar 

  34. Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering and System Safety 75(2), 167–177 (2002)

    Article  Google Scholar 

  35. Ruys, T.C.: Towards Effective Model Checking. PhD thesis, University of Twente (2001)

    Google Scholar 

  36. Schmidt, D.C.: Guest editor’s introduction: Model-driven engineering. IEEE Computer 39(2), 25–31 (2006)

    Article  Google Scholar 

  37. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  38. Sharp, C., Schaffert, S., Woo, A., Sastry, N., Karlof, C., Sastry, S., Culler, D.: Design and implementation of a sensor network system for vehicle tracking and autonomous interception. In: Proceedings of the 2nd European Workshop on Wireless Sensor Networks, pp. 93–107 (2005)

    Google Scholar 

  39. Sirigineedi, G., Tsourdos, A., White, B., Zbikowski, R.: Kripke modelling and model checking of a multiple UAV system monitoring road network. In: Proceedings of the AIAA Guidance, Navigation, and Control Conference (2010)

    Google Scholar 

  40. Tassey, G.: The economic impacts of inadequate infrastructure for software testing. Technical Report RTI Project Number 7007.011, National Institute of Standards and Technology (2002)

    Google Scholar 

  41. The Standish Group. CHAOS Chronicles Online (2007)

    Google Scholar 

  42. Tomlin, C.J., Mitchell, I., Bayen, A.M., Oishi, M.: Computational techniques for the verification of hybrid systems. Proceedings of the IEEE 91(7), 986–1001 (2003)

    Article  Google Scholar 

  43. Vardi, M.Y.: Branching vs. Linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  44. Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., Murray, R.M.: TuLiP: A software toolbox for receding horizon temporal logic planning. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, pp. 313–314 (2011)

    Google Scholar 

  45. Wooldridge, M.J., Ciancarini, P.: Agent-oriented software engineering: The state of the art. In: Ciancarini, P., Wooldridge, M.J. (eds.) AOSE 2000. LNCS, vol. 1957, pp. 1–28. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  46. Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT) 8(3), 216–228 (2006)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AFRL Control Science Center of Excellence, WPAFB, Brooks, OH, USA

    Laura R. Humphrey

Authors
  1. Laura R. Humphrey
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Laura R. Humphrey .

Editor information

Editors and Affiliations

  1. Computational Mathematics, North Randolph Street 875, Arlington, 22203, Virginia, USA

    Fariba Fahroo

  2. , ECE Dept., Wayne State University, Detroit, 48202, Michigan, USA

    Le Yi Wang

  3. , Department of Mathematics, Wayne State University, Detroit, 48202, Michigan, USA

    George Yin

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Humphrey, L.R. (2013). Model Checking for Verification in UAV Cooperative Control Applications. In: Fahroo, F., Wang, L., Yin, G. (eds) Recent Advances in Research on Unmanned Aerial Vehicles. Lecture Notes in Control and Information Sciences, vol 444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37694-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-37694-8_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-37693-1

  • Online ISBN: 978-3-642-37694-8

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation