Towards formalisation of 3D user interaction: Making spatial interaction verifiable

Abstract

Interactive systems which incorporate 3D interaction techniques, such as virtual or augmented reality, lack appropriate methods for formalisation to verify and validate their properties. In safety-critical contexts, such as virtual environments used for training users in medical settings, ensuring systems behave as expected is crucial to enabling positive user experiences. In this paper we propose a formalisation that will allow us to express 3D virtual environments, end users and their interactions. This work represents a first step towards creating formalisation methods for virtual reality applications, enabling model checking techniques to ensure systems behave as expected, leading to improved reliability, safety and better user experience in virtual environments.