Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

Published in:
Cover of the book

2019 | OriginalPaper | Chapter

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

Authors : Richard Banach, Joe Razavi, Suzanne Lesecq, Olivier Debicki, Nicolas Mareau, Julie Foucault, Marc Correvon, Gabriela Dudnik

Published in: Complex Systems Design & Management

Publisher: Springer International Publishing

share
SHARE

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.
Footnotes
1
In some niche areas, the recognition came as a direct result of painful and expensive failure, the Pentium Bug and Arianne Disaster being iconic examples.
 
2
It became apparent at this time that scalable formal tools were not an impossible dream, even if the degree of scalability was not as great as typically found in conventional approaches.
 
3
For reasons of the confidentiality of the future commercial exploitation of the INSPEX platform, what is shown here is not actual code.
 
Literature
2.
go back to reference Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996) Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)
3.
go back to reference Abrial, J.R.: Formal Methods in Industry: Achievements. Problems Future. In: Proceedings of ACM/IEEE ICSE 2006, pp. 761–768 (2006) Abrial, J.R.: Formal Methods in Industry: Achievements. Problems Future. In: Proceedings of ACM/IEEE ICSE 2006, pp. 761–768 (2006)
4.
go back to reference Abrial, J.R.: Modeling in Event-B: System and Software Engineering. CUP (2010) Abrial, J.R.: Modeling in Event-B: System and Software Engineering. CUP (2010)
5.
go back to reference 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) 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)
7.
go back to reference Baeten, J.: Process Algebra. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1990) Baeten, J.: Process Algebra. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1990)
8.
go back to reference Banach, R. (ed.): Special Issue on the State of the Art in Formal Methods. Journal of Universal Computer Science, vol. 13(5) (2007) Banach, R. (ed.): Special Issue on the State of the Art in Formal Methods. Journal of Universal Computer Science, vol. 13(5) (2007)
11.
go back to reference Bowen, J., Hinchey, M.: Seven more myths of formal methods. IEEE Software 12, 34–41 (1995) CrossRef Bowen, J., Hinchey, M.: Seven more myths of formal methods. IEEE Software 12, 34–41 (1995) CrossRef
12.
go back to reference Clarke, E., Wing, J.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28, 626–643 (1996) CrossRef Clarke, E., Wing, J.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28, 626–643 (1996) CrossRef
13.
go back to reference 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) CrossRef 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) CrossRef
14.
go back to reference 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) 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)
15.
go back to reference Fausten, M.: Evolution or revolution: architecture of AD cars. In: Proceedings of IEEE ESWEEK (2015) Fausten, M.: Evolution or revolution: architecture of AD cars. In: Proceedings of IEEE ESWEEK (2015)
17.
go back to reference Fitzgerald, J., Gorm Larsen, P.: Modelling Systems: Practical Tools and Techniques for Software Development. Cambridge University Press (1998) Fitzgerald, J., Gorm Larsen, P.: Modelling Systems: Practical Tools and Techniques for Software Development. Cambridge University Press (1998)
19.
20.
go back to reference Hoare, C.: Communicating Sequential Processes. Prentice-Hall (1985) Hoare, C.: Communicating Sequential Processes. Prentice-Hall (1985)
22.
go back to reference Jones, C.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall (1990) Jones, C.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall (1990)
23.
go back to reference Jones, C., O’Hearne, P., Woodcock, J.: Verified software: a grand challenge. IEEE Comput. 39(4), 93–95 (2006) CrossRef Jones, C., O’Hearne, P., Woodcock, J.: Verified software: a grand challenge. IEEE Comput. 39(4), 93–95 (2006) CrossRef
24.
go back to reference Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002) Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)
25.
go back to reference Mandruchi, R., Kurniavan, S.: Mobility-Related Accidents Experienced by People with Visual Impairment. Insight: Research and Practice in Visual Impairment and Blindness (2011) Mandruchi, R., Kurniavan, S.: Mobility-Related Accidents Experienced by People with Visual Impairment. Insight: Research and Practice in Visual Impairment and Blindness (2011)
26.
go back to reference Milner, R.: Communication and Concurrency. Prentice-Hall (1989) Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
28.
go back to reference Qu, Z.: Cooperative Control of Dynamical Systems: Applications to Autonomous Vehicles. Springer (2009) Qu, Z.: Cooperative Control of Dynamical Systems: Applications to Autonomous Vehicles. Springer (2009)
30.
go back to reference de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press (1998) de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press (1998)
31.
go back to reference Rosburg, T.: Tactile ground surface indicators in public places. In: Grunwald, M. (ed.) Human Haptic Perception: Basics and Applications. Springer, Birkhauser (2008) Rosburg, T.: Tactile ground surface indicators in public places. In: Grunwald, M. (ed.) Human Haptic Perception: Basics and Applications. Springer, Birkhauser (2008)
32.
go back to reference Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International (1992) Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International (1992)
33.
go back to reference Stepney, S.: New Horizons in Formal Methods. The Computer Bulletin, pp. 24–26 (2001) CrossRef Stepney, S.: New Horizons in Formal Methods. The Computer Bulletin, pp. 24–26 (2001) CrossRef
34.
go back to reference 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) 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)
35.
go back to reference Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics. MIT Press (2005) Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics. MIT Press (2005)
38.
go back to reference Woodcock, J.: First steps in the the verified software grand challenge. IEEE Computer 39(10), 57–64 (2006) CrossRef Woodcock, J.: First steps in the the verified software grand challenge. IEEE Computer 39(10), 57–64 (2006) CrossRef
39.
go back to reference Woodcock, J., Banach, R.: The verification grand challenge. JUCS 13, 661–668 (2007) Woodcock, J., Banach, R.: The verification grand challenge. JUCS 13, 661–668 (2007)
Metadata
Title
Formal Methods in Systems Integration: Deployment of Formal Techniques in INSPEX
Authors
Richard Banach
Joe Razavi
Suzanne Lesecq
Olivier Debicki
Nicolas Mareau
Julie Foucault
Marc Correvon
Gabriela Dudnik
Copyright Year
2019
DOI
https://doi.org/10.1007/978-3-030-04209-7_1

Premium Partners