Verifying the behaviour of virtual environment world objects

Abstract

Virtual environments are rapidly becoming more widespread and finding application outside specialised laboratories. However, there has been relatively little research developing tools and techniques to aid their development. This is particularly the case when defining the dynamics of the virtual world objects with which the user perceives and interacts. The complexity of these world objects can often mirror their real world counterparts, yet they are usually defined using program or macro application code. Consequently, there is no opportunity, beyond ad-hoc prototyping, of ensuring the world objects behave as required. Our work is focusing on the verification and refinement of abstract virtual environment behavioural specifications to an implementation. In this paper, we exemplify how the dynamics of these world objects can be specified using a hybrid formalism. We discuss and demonstrate how meaningful verification can take place on these specifications. © 2001 Springer-Verlag Berlin Heidelberg.