Formal and experimental validation approaches in HCI systems design based on a shared event B model

The development of user interfaces (UI) needs validation and verification of a set of required properties. Different kinds of properties are relevant to the human computer interaction (HCI) area. Not all of them may be checked using classical software engineering validation and verification tools. Indeed, a large part of properties is related to the user and to usability. Moreover, this kind of properties usually requires an experimental validation. This paper addresses the cooperation between formal and experimental HCI properties validation and verification. It focuses on a proof based technique (event B) and a Model Based System (MBS) based technique (SUIDT). Moreover, this paper tries to bridge the gap between both approaches in order to reduce the heterogeneity they lead to.