A Semantic Theory for Heterogeneous System Design

Rance Cleaveland and Gerald Luettgen

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


This paper develops a semantic theory for heterogeneous system designs in which some components are specified operationally and others are given logically. Using the traditional testing paradigm of DeNicola and Hennessy as a basis, the formalism introduces Buechi processes and Buechi tests with associated may- and must-preorders. These refinement orderings are then given alternative characterizations and shown to be conservative extensions of the relations studied by DeNicola and Hennessy. The paper also establishes a tight connection between the Buechi must-preorder and satisfaction of linear-time temporal logic (LTL) formulas by showing that a system satisfies an LTL formula if and only if it is larger than the Buechi process corresponding to the formula in the must-preorder. Consequently, the Buechi must-preorder permits a uniform treatment of traditional notions of process refinement and LTL satisfaction. It also provides an elegant semantic basis for heterogeneous system designs in which some system components are specified as labeled transition systems and others as LTL formulas. An example dealing with the design of a small communications protocol illustrates this point.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Maintainer fsttcs20@cse.iitd.ernet.in.
Start Conference Manager
Conference Systems