Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEX

Richard Banach, Joseph Razavi, Olivier Debicki , Suzanne Lesecq

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


Reviews of various kinds are an established part of system development, but rely on the vigilance and thoroughness of the human participants for their quality. The use of formal methods as part of the toolkit deployed during review can increase those elements of dependability that formal methods do best to support. A methodology that proposes that formal techniques are used alongside conventional system construction practices during review is introduced. These can reduce the human burden of ensuring review quality, even if the coupling between the formal and conventional strands is not itself formally enforced. The approach advocated was inspired by experience of the use of formal methods in the INSPEX Project.1 This project targets the creation of a minaturised smart obstacle detection system, to be clipped onto a visually impaired or blind (VIB) person’s white cane, that would give aural feedback to the user about obstacles in front of them. The increasing complexity of such systems itself invites the use of formal techniques during development, but the hardware challenges preclude the application of textbook top-down formal methods. The use of formal methods in INSPEX is ad hoc, and the methodology proposed is an abstraction from the practical experience.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science
Subtitle of host publicationFormal Methods
Publication statusAccepted/In press - 12 Aug 2019
EventFormal Methods 2019: Practical Formal Verification For Software Dependability - Porto, Portugal
Duration: 7 Oct 201911 Oct 2019


ConferenceFormal Methods 2019
Abbreviated titleAFFORD'19


Dive into the research topics of 'Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEX'. Together they form a unique fingerprint.

Cite this