Exploring Applications of Formal Methods in the INSPEX Project

As formal methods become increasingly practical, there is a need to explore their use in a variety of domains. Wearable sensing is a rapidly developing area in which formal methods can provide tangible benefits to end users, facilitating the advance of cutting-edge technology where consumer trust is critical. The INSPEX project aims to develop a miniaturized spatial exploration system incorporating multiple sensors and state of the art processing, initially focused on a navigation tool for visually impaired people. It is thus a useful test-case for formal methods in this domain. Applying formal methods in the INSPEX development process entailed adapting to realistic external pressures. The impact of these on the modelling process is described, attending in particular to the relationship between human and tool-supported reasoning.