Experience Report: Application of Falsification Methods on the UxAS System

  • Cumhur Erkan TuncaliEmail author
  • Bardh Hoxha
  • Guohui Ding
  • Georgios Fainekos
  • Sriram Sankaranarayanan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


In this report, we present our experiences in applying falsification methods over the Unmanned Systems Autonomy Services (UxAS) system. UxAS is a collection of software modules that enables complex mission planning for multiple vehicles. To test the system, we utilized the tool S-TaLiRo to generate mission scenarios for both UxAS and the underlying vehicle simulators, with the goal of finding behaviors which do not meet system specifications.


  1. 1.
    Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. (TECS) 12(2s), 95 (2013)Google Scholar
  2. 2.
    Air Force Research Laboratory, Aerospace System Directorate, Power and Control Division. OpenAMASE, Aerospace Multi-agent Simulation Environment, December 2017.
  3. 3.
    Air Force Research Laboratory, Aerospace System Directorate, Power and Control Division. OpenUXAS, Project for multi-UAV cooperative decision making, Dec. 2017. Available at
  4. 4.
    Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  5. 5.
    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Kingston, D., Rasmussen, S., Humphrey, L.: Automated UAV tasks for search and surveillance. In: 2016 IEEE Conference on Control Applications (CCA), pp. 1–8. IEEE (2016)Google Scholar
  7. 7.
    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRefGoogle Scholar
  8. 8.
    Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivancić, F., Gupta, A., Pappas, G.J.: Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: HSCC 2010, pp. 211–220. ACM, New York (2010)Google Scholar
  9. 9.
  10. 10.
    Sutton, M., Greene, A., Amini, P.: Fuzzing: Brute Force Vulnerability Discovery. Pearson Education, London (2007)Google Scholar
  11. 11.
    Tuncali, C.E., Yaghoubi, S., Pavlic, T.P., Fainekos, G.: Functional gradient descent optimization for automatic test case generation for vehicle controllers. In: 2017 IEEE International Conference on Automation Science and Engineering (CASE). IEEE (2017)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Arizona State UniversityTempeUSA
  2. 2.Southern Illinois UniversityCarbondaleUSA
  3. 3.University of ColoradoBoulderUSA

Personalised recommendations