Formal Development of Object-Based Systems in a Temporal Logic Setting

This paper presents TLO, an approach to the formal development of object-based systems in a temporal logic framework. The behavior of an object-based system is viewed as derivable from the behaviors of its constituent component objects. Temporal logic is a formalism well suited for specifying behavior of concurrent systems; it also provides conceptually simple notions of composition and refinement: Composition of objects is expressed as conjunction of the associated component specifications. The refinement relation between a low-level and a high-level specification requires that the former specification implies the latter.

Specifically in an object-based approach, systems and their components need to be viewed as open systems: Each object guarantees some service (behavior), provided its environment conforms to certain assumptions. Hence, such components are most appropriately specified in an assumption/guarantee style.

TLO adopts TLA as the underlying logical formalism. It encompasses a specification language for object-based designs and a corresponding method for specification and verification. The concepts are illustrated by an example involving both functional and fault-tolerance requirements.

Available as gzipped Postscript file (48 KB).

@inproceedings{Canver99:FDOBSTLS,
   author = "Canver, E. and von Henke, F.W.",
   title = "Formal Development of Object-Based Systems in a Temporal Logic Setting",
   booktitle = "Formal Methods for Open Object-Based Distributed Systems",
   pages = "419-436",
   editors = "Ciancarini, P. and Fantechi, A. and Gorrieri, R.",
   address = "Florence",
   organization = "IFIP",
   publisher = "Kluwer Academic Publishers",
   month = "February",
   year = "1999"
}