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

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.