kirancodes.me
To Proof Maintenance & Beyond!

The Specification and Testing of Quantified Progress Properties in Distributed Systems

Prakash Krishnamurthy, Paolo A. G. Sivilotti

Abstract

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.

BibTeX
@inproceedings{Krishnamurthy-Sivilotti:ICSE01,
  author    = {Prakash Krishnamurthy and
               Paolo A. G. Sivilotti},
  title     = {The Specification and Testing of Quantified Progress Properties in Distributed Systems},
  booktitle = {ICSE},
  pages     = {201--210},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Related papers