Advertisement

Formal Methods in Systems Integration: Deployment of Formal Techniques in INSPEX

  • Richard BanachEmail author
  • Joe Razavi
  • Suzanne Lesecq
  • Olivier Debicki
  • Nicolas Mareau
  • Julie Foucault
  • Marc Correvon
  • Gabriela Dudnik
Conference paper
First Online:

Abstract

Inspired by the abilities of contemporary autonomous vehicles to navigate with a high degree of effectiveness, the INSPEX Project aims to create a minaturised smart obstacle detection system, which could find use in a wide variety of leading edge smart applications. The primary use case focused on in the project is producing an advanced prototype for a device which can be attached to a visually impaired or blind (VIB) person’s white cane, and which, through the integration of a variety of minaturised sensors, and of the processing of their data via sophisticated algorithms, can offer the VIB user greater precision of information about their environment. The increasing complexity of such systems creates increasing challenges to assure their correct operation, inviting the introduction of formal techniques to aid in maximising system dependability. However, the major challenge to building such systems resides at the hardware end of the development. This impedes the routine application of top-down formal methods approaches. Some ingenuity must be brought to bear, in order that normally mutually hostile formal and mainstream approaches can contribute positively towards system dependability, rather than conflicting unproductively. This aspect is illustrated using two strands of the INSPEX Project.

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

Notes

Acknowledgement

Open image in new window This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 730953. The work was also supported in part by the Swiss Secretariat for Education, Research and Innovation (SERI) under Grant 16.0136 730953. We thank them for their support.

References

  1. 1.
  2. 2.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)Google Scholar
  3. 3.
    Abrial, J.R.: Formal Methods in Industry: Achievements. Problems Future. In: Proceedings of ACM/IEEE ICSE 2006, pp. 761–768 (2006)Google Scholar
  4. 4.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering. CUP (2010)Google Scholar
  5. 5.
    Andronick, J., Jeffery, R., Klein, G., Kolanski, R., Staples, M., Zhang, H., Zhu, L.: Large-scale formal verification in practice: a process perspective. In: Proceedings of ACM/IEEE ICSE 2012, pp. 374–393 (2012)Google Scholar
  6. 6.
  7. 7.
    Baeten, J.: Process Algebra. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1990)Google Scholar
  8. 8.
    Banach, R. (ed.): Special Issue on the State of the Art in Formal Methods. Journal of Universal Computer Science, vol. 13(5) (2007)Google Scholar
  9. 9.
  10. 10.
  11. 11.
    Bowen, J., Hinchey, M.: Seven more myths of formal methods. IEEE Software 12, 34–41 (1995)CrossRefGoogle Scholar
  12. 12.
    Clarke, E., Wing, J.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28, 626–643 (1996)CrossRefGoogle Scholar
  13. 13.
    Dia, R., Mottin, J., Rakotavao, T., Puschini, D., Lesecq, S.: Evaluation of occupancy grid resolution through a novel approach for inverse sensor modeling. In: Proceedings of IFAC World Congress, FAC-PapersOnLine, vol. 50, pp. 13,841–13,847 (2017)CrossRefGoogle Scholar
  14. 14.
    Divakaran, S., D’Souza, D., Kushwah, A., Sampath, P., Sridhar, N., Woodcock, J.: Refinement-based verification of the FreeRTOS scheduler in VCC. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) Proceedings of ICFEM 2015. LNCS, vol. 9407, pp. 170–186. Springer (2015)Google Scholar
  15. 15.
    Fausten, M.: Evolution or revolution: architecture of AD cars. In: Proceedings of IEEE ESWEEK (2015)Google Scholar
  16. 16.
  17. 17.
    Fitzgerald, J., Gorm Larsen, P.: Modelling Systems: Practical Tools and Techniques for Software Development. Cambridge University Press (1998)Google Scholar
  18. 18.
  19. 19.
    Hall, A.: Seven myths of formal methods. IEEE Software 7, 11–19 (1990)CrossRefGoogle Scholar
  20. 20.
    Hoare, C.: Communicating Sequential Processes. Prentice-Hall (1985)Google Scholar
  21. 21.
    ISO/IEC 13568: Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics: International Standard (2002). http://www.iso.org/iso/en/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip
  22. 22.
    Jones, C.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall (1990)Google Scholar
  23. 23.
    Jones, C., O’Hearne, P., Woodcock, J.: Verified software: a grand challenge. IEEE Comput. 39(4), 93–95 (2006)CrossRefGoogle Scholar
  24. 24.
    Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)Google Scholar
  25. 25.
    Mandruchi, R., Kurniavan, S.: Mobility-Related Accidents Experienced by People with Visual Impairment. Insight: Research and Practice in Visual Impairment and Blindness (2011)Google Scholar
  26. 26.
    Milner, R.: Communication and Concurrency. Prentice-Hall (1989)Google Scholar
  27. 27.
  28. 28.
    Qu, Z.: Cooperative Control of Dynamical Systems: Applications to Autonomous Vehicles. Springer (2009)Google Scholar
  29. 29.
  30. 30.
    de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press (1998)Google Scholar
  31. 31.
    Rosburg, T.: Tactile ground surface indicators in public places. In: Grunwald, M. (ed.) Human Haptic Perception: Basics and Applications. Springer, Birkhauser (2008)Google Scholar
  32. 32.
    Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International (1992)Google Scholar
  33. 33.
    Stepney, S.: New Horizons in Formal Methods. The Computer Bulletin, pp. 24–26 (2001)CrossRefGoogle Scholar
  34. 34.
    Stepney, S., Cooper, D.: Formal Methods for Industrial Products. In: Proceedings of 1st Conference of B and Z Users. LNCS, vol. 1878, pp. 374–393. Springer (2000)Google Scholar
  35. 35.
    Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics. MIT Press (2005)Google Scholar
  36. 36.
  37. 37.
    Wikipedia: List of tools for static code analysis. https://en.wikipedia.org/wiki/List_of_tools_ for_static_code_analysis
  38. 38.
    Woodcock, J.: First steps in the the verified software grand challenge. IEEE Computer 39(10), 57–64 (2006)CrossRefGoogle Scholar
  39. 39.
    Woodcock, J., Banach, R.: The verification grand challenge. JUCS 13, 661–668 (2007)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Richard Banach
    • 1
    Email author
  • Joe Razavi
    • 1
  • Suzanne Lesecq
    • 2
  • Olivier Debicki
    • 2
  • Nicolas Mareau
    • 2
  • Julie Foucault
    • 2
  • Marc Correvon
    • 3
  • Gabriela Dudnik
    • 3
  1. 1.School of Computer ScienceUniversity of ManchesterManchesterUK
  2. 2.CEA, LETI, Minatec CampusGrenoble CedexFrance
  3. 3.CSEM SANeuchatelSwitzerland

Personalised recommendations

Cite paper

Buy options