Refinement Based Formal Development of Human-Machine Interface

Human factors have been considered as the most common causes of accidents, particularly for interacting with complex critical systems related to avionics, railway, nuclear and medical domains. Mostly, a human-machine interface (HMI) is developed independently and the correctness of possible interactions is heavily dependent on testing, which cannot guarantee the absence of run-time errors. The use of formal methods in HMI development may assure such guarantee. This paper presents a methodology for developing an HMI using a correct by construction approach, which allows us to introduce the HMI components, functional behaviour and the required safety properties progressively. The proposed methodology, generic refinement strategy, supports a development of the model-view-controller (MVC) architecture. The whole approach is formalized using Event-B and relies on the Rodin tools to check the internal consistency with respect to the given safety properties, invariants and events. Finally, an industrial case study is used to illustrate the effectiveness of our proposed approach for developing an HMI.