Physical interfaces have been widely adopted in digital games. In our project, we research one such type of physical interface---handheld augmented reality interfaces, and aim to create an engaging and novel play experience. Designing such games requires us to combine knowledge from both Human-computer interaction and game design domains. In this paper, we present a few research questions that we raised or encountered during the process of designing and developing the handheld AR game NerdHerder. We also present our current solutions and answers to these questions. We are going to conduct user studies to understand how handheld AR games are played in the wild. We will release the game and let mobile device users play it in their natural environments. Through the process of designing and iterating NerdHerder, we call for more research that explores how to adopt HCI principles into game design.

The hardware and software in modern aircraft control systems are good candidates for verification using formal methods: they are complex, safety-critical, and challenge the capabilities of test-based verification strategies. We have previously reported on our use of model checking to verify the time partitioning property of the Deos/spl trade/ real-time operating system for embedded avionics. The size and complexity of this system have limited us to analyzing only one configuration at a time. To overcome this limit and generalize our analysis to arbitrary configurations we have turned to theorem proving. This paper describes our use of the PVS theorem prover to analyze the Deos scheduler. In addition to our inductive proof of the time partitioning invariant, we present a feature-based technique for modeling state-transition systems and formulating inductive invariants. This technique facilitates an incremental approach to theorem proving that scales well to models of increasing complexity, and has the potential to be applicable to a wide range of problems.

We present a versatile statistical verification methodology and we illustrate different uses of this methodology on two examples of nonlinear real-time UAV controllers. The first example applies our statistical methodology to the verification of a computation time property for a software implementation of a high-performance controller as a function of controller state variable values. The second example illustrates our statistical verification methodology applied to finding verifiably safe flight envelopes for a class of maneuvers, again as a function of controller state variable values. We compare our approach to verification with other statistical techniques used for estimating execution times and controller performance. We close with candidate topics for future work.

Technology transfer is an especially difficult proposition for real-time control. To facilitate it, we need to complement the “high-performance” orientation of control research with an emphasis on establishing “high confidence” in real-time implementation. Two particular problems are discussed and recent research directed at their solutions is presented. First, the use of anytime algorithms requires dynamic resource management technology that generally is not available today in real-time systems. Second, complex algorithms have unpredictable computational characteristics that, nevertheless, need to be modeled; statistical verification is suggested as a possible approach. In both cases, a synthesis of control engineering and computer science is required if effective solutions are to be devised. Simulation-based demonstrations with uninhabited aerial vehicles (UAVs) serve to illustrate the research efforts. © 2004 Wiley Periodicals, Inc.