The specification and testing of quantified progress properties in distributed systems

There are two basic parts to the behavioral specification of distributed systems: safety and progress. In earlier work, we developed a tool to monitor progress properties of CORBA components specified using the temporal operator transient. In this paper, we address the specification and testing of transient properties that are quantified (over both bounded and unbounded domains). We categorize typical quantifications that arise in practical systems and discuss possible implementation strategies. We define functional transients, a subclass of quantified transient properties that can be monitored in constant space and time. We outline the design and implementation of a tool for testing these properties in CORBA components.