In this paper we present an account of children's interactions with a mobile technology prototype within a school context. The Noise Detectives trial was conducted in a school setting with the aim of better understanding the role of mobile technology as a mediator within science learning activities. Over eighty children, aged between ten and twelve, completed an outdoor data gathering activity using a mobile learning prototype that included paper and digital components. They measured and recorded noise levels at a range of locations throughout the schools. We analyzed the activity to determine how the components of the prototype were integrated into the learning activity, and to identify differences in behavior that resulted from using these components. We present design implications that resulted from observed differences in prototype use and appropriation.

In this paper we discuss the use of models of space in the building of mixed-reality systems. By model of space we mean a geometric or symbolic description associated with a physical space. We outline several types of model that exist, how they are surveyed and authored, how they are represented to the users and how they are supported by middleware and sensors. We show that systems often contain numerous models of space and we discuss the issues in maintaining or reifying assumptions about transformations between models. We illustrate these ideas by describing the implementation of a collaborative mixed-reality system that allows users to experience a museum in three modalities: physically colocated visitor with personal digital assistant guide, virtual reality visitor and Web visitor.

Museums attract increasing numbers of online visitors along with their conventional physical visitors. This paper presents a study of a mixed reality system that allows web, virtual reality and physical visitors to share a museum visit together in real time. Our system allows visitors to share their location and orientation, communicate over a voice channel, and jointly navigate around a shared information space. Results from a study of 34 users of the system show that visiting with the system was highly interactive and retained many of the attractions of a traditional shared exhibition visit. Specifically, users could navigate together, collaborate around objects and discuss exhibits. These findings have implications for non-museum settings, in particular how location awareness is a powerful resource for collaboration, and how 'hybrid objects' can support collaboration at-a-distance.

We define a translation from the User Action Notation (UAN) to the process algebra Communicating Sequential Processes (CSP). UAN is an informal notation, used for task modeling and design. Translating a UAN task description to CSP provides a base for rigorous development of an interactive system. The resulting CSP description is a suitable abstract starting point for development, as it describes externally visible behaviour with no mention of presented or underlying state. Our translation covers all UAN constructs except for waiting, interruptibility and true concurrency which cannot be expressed in interleaving, un-timed CSP. Our approach integrates task models, typically based on user-oriented concerns, into rigorous development which is typically system-oriented. It provides a bases for a framework for formal development of interactive systems.

This paper describes a method for specification-based class testing that incorporates test case generation, execution, and evaluation based on formal specifications. This work builds on previous achievements in the areas of specification-based testing and class testing by integrating the two within a single framework. The initial step of the method is to generate test templates for individual operations from a specification written in the Object-Z specification language. These test templates are combined to produce a finite state machine for the class that is used as the basis for test case execution using the ClassBench test execution framework. An oracle derived from the Object-Z specification is used to evaluate the outputs. The method is explained using a simple example and its application to a more substantial case study is also discussed. Keywords: specification-based testing, Object-Z, class testing, ClassBench, oracles 1

The paper contains a case study demonstrating a complete process for specification based class testing. The process starts with an abstract specification written in Object-Z and concludes by exercising an implementation with test cases and evaluating the results. The test cases are derived using the Test Template Framework for each individual operation. They are analysed to generate a finite state machine that can execute test sequences within the ClassBench framework. An oracle is also derived from the Object-Z specification. The case study demonstrates how a formal specification contributes to the development of practical tests that can be executed by a testing tool. It also shows how a test oracle can be derived from a specification and used by the same testing tool to evaluate test results.