Integrating Formal Verification and Assurance: An Inspection Rover Case Study | SpringerLink
Skip to main content
Springer Nature Link
Log in

Integrating Formal Verification and Assurance: An Inspection Rover Case Study

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12673))

Included in the following conference series:

Abstract

The complexity and flexibility of autonomous robotic systems necessitates a range of distinct verification tools. This presents new challenges not only for design verification but also for assurance approaches. Combining the distinct formal verification tools, while maintaining sufficient formal coherence to provide compelling assurance evidence is difficult, often being abandoned for less formal approaches. In this paper we demonstrate, through a case study, how a variety of distinct formal techniques can be brought together in order to develop a justifiable assurance case. We use the AdvoCATE assurance case tool to guide our analyses and to integrate the artifacts from the formal methods that we use, namely: fret, cocosim and Event-B. While we present our methodology as applied to a specific Inspection Rover case study, we believe that this combination provides benefits in maintaining coherent formal links across development and assurance processes for a wide range of autonomous robotic systems.

Work supported by NASA ARMD System-Wide Safety Project, UK Research and Innovation and EPSRC Hubs for “Robotics and AI in Hazardous Environments”: EP/R026092 (FAIR-SPACE), and the Royal Academy of Engineering.

The authors thank Dimitra Giannakopoulou for her valuable feedback on this work.

M. Farrell—Majority of Farrell’s work took place at the Universities of Liverpool & Manchester.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 9723
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 12154
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    UKRI and EPSRC Hubs for “Robotics and AI in Hazardous Environments”.

References

  1. GSN Community Standard Version 2. Technical report, Assurance Case Working Group of The Safety-Critical Systems Club (Jan 2018)

    Google Scholar 

  2. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Google Scholar 

  3. Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010)

    Article  Google Scholar 

  4. Banach, R.: Hemodialysis machine in hybrid event-B. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 376–393. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_32

    Chapter  Google Scholar 

  5. Bourbouh, H., Farrell, M., Mavridou, A., Sljivo, I.: Integration and Evaluation of the Advocate, FRET, CoCoSim, and Event-B Tools on the Inspection Rover Case Study. Technical report, TM-2020-5011049, NASA (2021)

    Google Scholar 

  6. Bourbouh, H., Garoche, P.-L., Loquen, T.,É, Noulard, T., Pagetti, C.: CoCoSim, a code generation framework for control/command applications: an overview of CoCoSim for multi-periodic discrete simulink models. In: European Congress on Embedded Real Time Software and Systems (2020)

    Google Scholar 

  7. Cardoso, R.C., Dennis, L.A., Farrell, M., Fisher, M., Luckcuck, M.: Towards compositional verification for modular robotic systems. In: Workshop on Formal Methods for Autonomous Systems, pp. 15–22. Electronic Proceedings in Theoretical Computer Science (2020)

    Google Scholar 

  8. Cardoso, R.C., Farrell, M., Luckcuck, M., Ferrando, A., Fisher, M.: Heterogeneous verification of an autonomous curiosity rover. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 353–360. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-55754-6_20

    Chapter  Google Scholar 

  9. Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 510–517. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_29

    Chapter  Google Scholar 

  10. Christakis, M., Müller, P., Wüstholz, V.: Collaborative verification and testing with explicit assumptions. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 132–146. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_13

    Chapter  Google Scholar 

  11. Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: International Conference on Automated Software Engineering, pp. 702–705. IEEE (2013)

    Google Scholar 

  12. CoCoSim-Team. CoCoSim - Automated Analysis Framework for Simulink. https://github.com/NASA-SW-VnV/CoCoSim

  13. Denney, E., Pai, G.: Automating the assembly of aviation safety cases. IEEE Trans. Reliab. 63(4), 830–849 (2014)

    Article  Google Scholar 

  14. Denney, E., Pai, G.: Safety case patterns: theory and applications. NASA/TM2015218492 (2015)

    Google Scholar 

  15. Denney, E., Pai, G.: Architecting a safety case for UAS flight operations. In: International System Safety Conference, vol. 12 (2016)

    Google Scholar 

  16. Denney, E., Pai, G.: Tool support for assurance case development. Autom. Softw. Eng. 25(3), 435–499 (2017). https://doi.org/10.1007/s10515-017-0230-5

    Article  Google Scholar 

  17. Dennis, L.A., Farwer, B.: Gwendolen: a BDI language for verifiable agents. In: Workshop on Logic and the Simulation of Interaction and Reasoning, pp. 16–23. AISB (2008)

    Google Scholar 

  18. Dezfuli, H., et al.: NASA system safety handbook. Volume 2: System Safety Concepts, Guidelines, and Implementation Examples (2015)

    Google Scholar 

  19. Farrell, M., Luckcuck, M., Fisher, M.: Robotics and integrated formal methods: necessity meets opportunity. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 161–171. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_10

    Chapter  Google Scholar 

  20. Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8

    Chapter  Google Scholar 

  21. Foster, S.D., Nemouchi, Y., O’Halloran, C., Tudor, N., Stephenson, K.: Formal model-based assurance cases in Isabelle/SACM: an autonomous underwater vehicle case study. In: Formal Methods in Software Engineering. ACM (2020)

    Google Scholar 

  22. FRET-Team. FRET - Formal Requirements Elicitation Tool. https://github.com/NASA-SW-VnV/FRET

  23. Giannakopoulou, D., Mavridou, A., Pressburger, T., Rhein, J., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. Foundation for software quality (Demo-Track). In: Requirements Engineering (2020)

    Google Scholar 

  24. Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Generation of formal requirements from structured natural language. In: Madhavji, N., Pasquale, L., Ferrari, A., Gnesi, S. (eds.) REFSQ 2020. LNCS, vol. 12045, pp. 19–35. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44429-7_2

    Chapter  Google Scholar 

  25. Gleirscher, M., Foster, S., Nemouchi, Y.: Evolution of formal model-based assurance cases for autonomous robots. In: Ölveczky, P.C., Salaün, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 87–104. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30446-1_5

    Chapter  Google Scholar 

  26. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305–1320 (1991)

    Article  Google Scholar 

  27. Kelly, J.C.: Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems Volume II: A Practitioner’s Companion (1997)

    Google Scholar 

  28. Le, V.H., Correnson, L., Signoles, J., Wiels, V.: Verification coverage for combining test and proof. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 120–138. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92994-1_7

    Chapter  Google Scholar 

  29. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  MATH  Google Scholar 

  30. Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. (CSUR) 52(5), 1–41 (2019)

    Article  Google Scholar 

  31. Mammar, A., Laleau, R.: Modeling a landing gear system in event-B. Int. J. Softw. Tools Technol. Transfer 19(2), 167–186 (2017)

    Article  Google Scholar 

  32. Maurica, F., Cok, D.R., Signoles, J.: Runtime assertion checking and static verification: collaborative partners. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018, Part II. LNCS, vol. 11245, pp. 75–91. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_6

    Chapter  Google Scholar 

  33. Mavridou, A., Bourbouh, H., Garoche, P.-L., Giannakopoulou, D., Pressburger, T., Schumann, J.: Bridging the gap between requirements and Simulink model analysis. In: International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020, Poster) (2020)

    Google Scholar 

  34. Mavridou, A., Bourbouh, H., Garoche, P.-L., Hejase, M.: Evaluation of the FRET and CoCoSim tools on the ten Lockheed Martin Cyber-Physical challenge problems. Technical report, TM-2019-220374, NASA (2019)

    Google Scholar 

  35. Mavridou, A., et al.: The ten lockheed martin cyber-physical challenges: formalized, analyzed, and explained. In: International Requirements Engineering Conference (RE), pp. 300–310. IEEE (2020)

    Google Scholar 

  36. McComas, D.: NASA/GSFC’s flight software core flight system. In: Flight Software Workshop, vol. 11 (2012)

    Google Scholar 

  37. Méry, D., Singh, N.K.: Formal development and automatic code generation: cardiac pacemaker. In: International Conference on Computers and Advanced Technology in Education (2011)

    Google Scholar 

  38. Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.: Compositional verification of a medical device system. In: SIGAda Annual Conference on High Integrity Language Technology, pp. 51–64 (2013)

    Google Scholar 

  39. Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software, vol. 3, p. 5 (2009)

    Google Scholar 

  40. Rivera, V., Cataño, N.: Translating event-B to JML-specified Java programs. In: ACM Symposium on Applied Computing, pp. 1264–1271 (2014)

    Google Scholar 

  41. Schneider, S., Treharne, H., Wehrheim, H.: A CSP approach to control in event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 260–274. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16265-7_19

    Chapter  Google Scholar 

  42. Sljivo, I., Gallina, B., Carlson, J., Hansson, H., Puri, S.: Tool-supported safety-relevant component reuse: from specification to argumentation. In: Casimiro, A., Ferreira, P.M. (eds.) Ada-Europe 2018. LNCS, vol. 10873, pp. 19–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92432-8_2

    Chapter  Google Scholar 

  43. Stamatis, D.H.: Failure Mode and Effect Analysis: FMEA from Theory to Execution. Quality Press, Milwaukee (2003)

    Google Scholar 

  44. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48153-2_6

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. KBR/NASA Ames Research Center, Mountain View, USA

    Hamza Bourbouh, Anastasia Mavridou & Irfan Sljivo

  2. NASA Ames Research Center, Mountain View, USA

    Guillaume Brat

  3. Department of Computer Science, Maynooth University, Maynooth, Ireland

    Marie Farrell

  4. Department of Computer Science, University of Manchester, Manchester, UK

    Louise A. Dennis & Michael Fisher

Authors
  1. Hamza Bourbouh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marie Farrell
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anastasia Mavridou
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Irfan Sljivo
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Guillaume Brat
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Louise A. Dennis
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Michael Fisher
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marie Farrell .

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, Hampton, VA, USA

    Aaron Dutle

  2. National Institute of Aerospace, Hampton, VA, USA

    Mariano M. Moscato

  3. National Institute of Aerospace, Hampton, VA, USA

    Laura Titolo

  4. NASA Langley Research Center, Hampton, VA, USA

    César A. Muñoz

  5. National Institute of Aerospace, Hampton, VA, USA

    Ivan Perez

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bourbouh, H. et al. (2021). Integrating Formal Verification and Assurance: An Inspection Rover Case Study. In: Dutle, A., Moscato, M.M., Titolo, L., Muñoz, C.A., Perez, I. (eds) NASA Formal Methods. NFM 2021. Lecture Notes in Computer Science(), vol 12673. Springer, Cham. https://doi.org/10.1007/978-3-030-76384-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-76384-8_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-76383-1

  • Online ISBN: 978-3-030-76384-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation