In: Proc. 19th Int. Conf. on Software Engineering, 19-25 April 1998, Kyoto, Japan, pages 33-42. 1997. ISBN 0-8186-8368-6, IEEE CS No. PR08368, IEEE Catalog No. 98CB36139.
Abstract: The design, implementation, and testing of virtual environments is complicated by the concurrency and real-time features of these systems. Therefore, the development of formal methods for modeling and analysis of virtual environments is highly desirable. In the past, Petri net models have led to good empirical results in the automatic verification of concurrent and real-time systems. An extension of time Petri nets is applied to modeling and analysis of the CAVE virtual environments at the University of Illinois at Chicago. This paper reports on the time Petri net model and on empirical studies conducted with the Cabernet toolset from Politecnico di Milano. The experiments uncovered a flaw in the way a shared buffer is used by CAVE processes. Due to an erroneous synchronization on the buffer, different CAVE walls can simultaneously display images based on different input information. The conclusion is that Petri net based tools can effectively support the development of reliable virtual environments.
Keywords: CABERNET, CAVE, time Petri nets, virtual environments.
Back to the Petri Nets Bibliography