Passive Mid-Stream Monitoring of Real-Time Properties

We present an approach for passively monitoring a large class of real-time behaviors of systems, by observing the mid-stream behavior of the system and without influencing the inputs to the system. Our approach is based on timed automata, and extends the untimed passive monitoring approach of [13]. We have implemented our approach using the real-time model checker UPPAAL, and we describe the application of our approach to passively test fault tolerance software in a telecommunications switch deeveloped at Lucent Technologies.