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.