Formal methods by stealth: The INSPEX experience. Issue 12 (13th October 2021)

• Record Type: Journal Article
• Authors: Banach, Richard; Razavi, Joseph; Debicki, Oivier; Lesecq, Suzanne
• Is Part Of: Journal of software. Volume 33:Issue 12(2021)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2021-10-13
• Subjects: dependability -- event‐B -- formal methods -- INSPEX -- obstacle detection systems -- PRISM -- ProB -- Rodin -- visually impaired or blind; Software engineering -- Periodicals; Computer software -- Development -- Periodicals; Software maintenance -- Periodicals; 005.1
• DOI: 10.1002/smr.2383
• Languages: English
• ISSNs: 2047-7473

Abstract

Abstract: 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, for example, 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. Abstract : The INSPEX Project, to design and integrate a number of sensors to create a minaturised obstacle location device, was of sufficient complexity to merit the use of formal methods. These were deployed in data pathway verification, and in power management design. A flexible, ad hoc approach to the use of formal methods was vital in their successful contribution to the project.