next up previous
Next: Related Work Up: Interface-Based Protocol Specification of Previous: Describing Interactions

Foundations

   

PSL constructs are based on structures describing possible worlds, as found in model theory and temporal and modal logic[31,19,64]. These serve as the basis for several frameworks for specifying possibly distributed systems [38,42,14,34,6], as well as related applied temporal reasoning systems in AI and object-oriented logic programming [43,3,15].

Possible world structures are of the form <W, V, R>. W is a set of worlds. V is a set of value expressions over some basis, with an associated function (p, w), which is true if expression p holds in world w. R represents any number of defined relations among the worlds in W. Chief among them is the relation generated by constraints. PSL rules define the set of all worlds that are possible, and a corresponding relation containing every pair of possible worlds.

PSL situations define a another family of ``static'' equivalence relations R. Situation S describes that set of worlds for which its defining predicate P holds given the values in the world (i.e., {w (P ,w)}). In PSL this is expressed in terms of the matching relation, , between values holding in worlds and situation predicates. The corresponding relation R contains all pairs of worlds that are members of this set.

The relation R serves as the basis for PSL ordering operators. This relation is simplest to describe formally when expressions are restricted to event predicates on fixed messages[23,67,57]. In this case, expressions in V are just characteristic predicates of sets of event occurrences, and (e,w) is true if w contains the events of e. For example, suppose a satisfies e = out(m1) for some message m1, and b satisfies e = out(m1) && in(m1). The relation a b states that e e. The out(m1) event has not ``gone away'' in B. In fact, if a b, out(m1) holds no later than the realization in which in(m1) holds as well. Thus, when restricted to events, the relation R contains all (a,b) such that the set of events described by must be be a subset of that described by e. When expressions are liberalized to allow reference to arbitrary attributes, the relation is no longer definable in this semi-automatic manner, since it is not necessarily the case that e e. Constraint rules must be supplied to describe how arbitrary attributes vary with respect to events.

Application of these constructs to particular systems relies on mappings from PSL to concrete implementation code and/or observations. These include (1) mappings between roles and implementation objects; (2) mappings between event predicates and concrete communication occurrences; (3) mappings between expressions defining situations and realizations observed or inferred in concrete code and/or its execution; and in some cases (4) mappings of the initial conditions of the system of interest. These generate an operational semantics that in turn allows construction of corresponding design methods and tools; for example simulation, prototyping, verification, visualization, testing, and monitoring. This also allows PSL to be used as a scripting language in which prococol specifications are directly compiled into default implementations.

While the use of PSL in some systems would require development of auxiliary configuration languages and tools to establish mappings, the particular features of PSL/IDL along with those of CORBA permit simpler tactics: PSL/IDL uses the same value type system as CORBA IDL. OMG standards in turn already map IDL value types to those of various implementation languages [54]. PSL/IDL message types map directly to those used in CORBA. Observations of messages may be used to establish instantiation of corresponding event predicates. Also CORBA Object Request Brokers (ORBs) and repositories maintain information relating values that are used as message destinations and the locations of concrete implementation components. These may be relied on to maintain implicit mappings between interface instance handles and implementation objects. And the initial conditions of most CORBA applications amount only to the initialization of a small number of components, avoiding the need for extensive description of static configuration properties.

CORBA also supports development of the instrumentation needed for dynamic execution tools. Event monitoring may be accomplished through interpositioning; the placement of intercepts between communicating components to tap communication traffic[68]. However, even if attention is restricted to event predicates, mapping communications to event predicates, and in turn realizations of particular situations, and in turn rule instantiations is not a trivial matter in a distributed open system (see [39]). However, provided that such observational apparatus is available, one could create, for example, a monitoring tool reporting whether realizations matching listed situations occurred and whether the corresponding ordering rules were observed.


next up previous
Next: Related Work Up: Interface-Based Protocol Specification of Previous: Describing Interactions


Doug Lea@Fri Mar 17 08:19:23 EST 1995