Modeling and analysis of a virtual reality system with time Petri nets
Rajesh Mascarenhas, Dinkar Karumuri, Ugo A. Buy, Robert V. Kenyon · 1998
The design, implementation, and testing of virtual en-vironments is complicated by the concurrency and real-time features of these systems. Therefore, the develop-ment of formal methods for modeling and analysis of virtual environments is highly desirable. In the paat, Petri-net models have led to good empirical results in the automatic verification of concurrent and real-time systems. We applied a timed extension of Petri nets to modeling and analysis of the CAVETM 1 virtual envi-ronment at the University of Illinois at Chicago. Here, we report on our time Petri net model and on empirical studies that we conducted with the Cabernet toolset from Politecnico di Milano. Our experiments uncov-ered a flaw in the way a shared buffer is used by CAVE processes. Due to an erroneous synchronization on the buffer, different CAJ’E walls can simultaneously display images based on different input information. We con-clude from our empirical studies that Petri-net-based tools can effectively support the development of reliable virtual environments.