We report on a display system to support laparoscopy by loosely coupling input sensors (e.g., cameras) with outputs (e.g., image displays). A low-latency and general-purpose computing platform is inserted between the traditionally tightly-coupled inputs and outputs of a laparoscopic surgical environment. The architecture of the proposed system provides flexibility in the fusion and augmentation of multiple input data sources and in the display of the data on a scalable large display. The performance of the described system is measured. The result indicates that our system has great potential to improve the performance of laparoscopic surgeons.

Radio frequency identification (RFlD) is a technology for automatically tracking the location of persons and objects tagged with a small radio transceiver. Its use in retail and security applications has received widespread attention in the popular press, RFID's application in hospital business processes is increasing rapidly, and a number of safety-critical clinical applications have been prototyped. In order to determine RFID 's fitness for use in safety-critical as well as more mundane perioperative processes, the operating room of the future project at the University of Maryland Medical Center evaluated six active-RFID systems. The evaluation consisted of hands-on testing of a variety of COTS systems employing the leading active-RFID technologies-802.11 RF, proprietary RF, ultra-wideband, infrared and ultrasound. In this paper we report the results of those tests and discuss their implications for the application of active-RFID technology to clinical applications

The paper discusses the use of formal methods for the analysis of architectural models expressed in the modeling language AADL. AADL describes the system as a collection of interacting components. The AADL standard prescribes semantics for the thread components and rules of interaction between threads and other components in the system. We present a semantics-preserving translation of AADL models into the real-time process algebra ACSR, allowing us to perform schedulability analysis of AADL models

We report on a tool we have developed that automates the derivation of tests from specifications. The tool implements conformance testing techniques to derive symbolic tests that incorporate their own oracles from formal operational specifications. It was applied for testing a simple version of the CEPS (Common Electronic Purse Specification).

Formal methods approaches to software and hardware verification use mathematical models and rigorous proof techniques to describe and analyze system models. Though most formalisms will allow models of unlimited complexity to be constructed, rigorous analysis of realistic models is frequently intractable. In this paper we describe the Algebra of Communicating Shared Resources with Value Passing (ACSR-VP), a process algebra for modeling resource-bound real-time systems, and describe how we are using testing techniques to check functional and real-time properties of realistic systems. Though testing based analysis lacks the certainty of formal analysis, it significantly expands the size of models that can be considered.

Verifying timing properties of real-time systems by tradi-