Formal Methods by Stealth: The INSPEX Experience

INSPEX is an INtegrated Smart sPatial EXploration system. It relies on a family of sensors, like automated
vehicles do, to provide enough information to a digital system for it to make reliable inferences
about the location of obstacles and other impediments in its environment. Unlike the automated vehicle
case, INSPEX is minaturised, because it is intended for lightweight applications and for portable use by
humans, e.g. visually impaired persons navigating outdoors (among many similar use cases). The complexity
of this hardware-focused system merited the introduction of formal methods during its (essentially
conventionally structured) development. The aim was to improve the dependability of parts of the implemented
system, and to estimate system characteristics via modelling and calculation that could not be
obtained experimentally within the scope of the project. The paper overviews the experience of the very
much human-in-the-loop use of formal techniques in the INSPEX project, and focuses particularly on the
human issues that impacted the cooperation between the conventional techniques and formal methods.