next up previous
Next: Related Work Up: PSL: Protocols and Pragmatics Previous: Examples

Methods and Tools

 

PSL may be used to support a number of development practices and engineering tools:

Monitoring.

Recordings of freely executing ``live'' components may check whether and how often a given set of actual components obey a particular protocol over some period of interest. Simple monitoring tools merely record event histories for later checks that they conform to stated protocols. More sophisticated monitoring agents perform conformance checks in real-time during the lifetime of the system. Monitors may also be attached to protocol visualization tools that allow developers to ``see'' the realizations of a protocol as they unfold within implementations. Interactive monitoring may be extended to create debuggers allowing users to construct new entities, issue new events, and/or alter existing ones in a live system.

Testing.

Recordings of components from a fixed initial configuration check whether protocols are obeyed and/or particular terminal situations are reached. Protocol rules may also guide construction of a test suite that covers all listed paths and situations defined in a given protocol. Additionally, they may be used to dynamically evaluate existing or randomized tests, checking that all paths have been covered.

Verification.

Analytic, symbolic checks (at various levels of formality) determine whether implementations possess required properties. Given a set of specifications and an implementation, verification efforts analytically decide whether the implementation conforms to the specification.

Design for testability.

Specification-guided programming (also known as ``reification'' [19]) is the process of ``deriving'' concrete implementations from their specifications. Reification typically involves substantial refinement, narrowing down interfaces and protocols to reflect various design constraints. In addition to required operations, implementations may also compute or approximate attribute functions and expressions on attributes found in specifications. This provides a simpler basis for testing, enhances the likelihood that implementations of other operations are correct ``by construction'', and enables ``reflective'' programming practices in which components inspect their own logical state. However, even the most detailed open specifications do not completely determine their implementations. For example, even when a PSL specification boils down to mandating that a given component rely on another with the properties of a simple int variable, this might not preclude an implementation using a special kind of C++ object that behaves as an int but also periodically logs its value to persistent media.

Design recovery.

Recovery is the reverse of reification: retrospectively ``deriving'' specifications by abstracting over implementation choices. Design recovery may also involve translation from or to less formal design documentation, as well as validation efforts, comparing specifications against high-level requirements.

Simulation and prototyping.

Semi-automated partial implementation, using a set of default strategies for minimally implementing those features of roles, events, and attributes of interest may be used to investigate system behavior.

Mappings

While PSL represents the core, it is only one piece of a unified approach to the specification of open systems. A complete account requires models, languages, and/or tools that map these abstractions to concrete features of particular systems. All of the above applications rely upon mappings relating any given specification to code that may conform to it. These mappings naturally vary across the languages, tools, and infrastructures used to implement a system:

  1. Mappings between roles and implementation objects (components).
  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.

Additionally, several of these applications require descriptions of certain initial conditions of the system of interest.

The need for, nature, and use of mappings differs across these kinds of applications. At one extreme lie formal verification efforts. Analytic verification requires a rigorous mapping to the underlying target programming languages, systems, and tools in order to construct an operational semantics [30]. Such a mapping is often impossible in practice, in large part because properties of implementation languages, libraries, and tools are not known in sufficient detail. Moreover, even when implementations are produced in well-behaved languages, full systems-level verification is often an unrealistic, intractable goal.

Simple visualization tools lie at the other extreme. A useful visualization tool might require only a mapping from events to observable messages, ignoring all other aspects of PSL expressions, at the price of not being able to distinguish two situations containing the same event predicates but different attribute predicates.

Mapping PSL/IDL

We illustrate some general mapping issues with PSL/IDL. While the use of PSL in some systems requires development of auxiliary configuration languages and tools to establish mappings, the particular features of PSL/IDL along with those of CORBA permit simpler tactics:

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 [71]. CORBA allows ``listener'' objects to be interposed along any communications path by transparently altering the mappings between roles and implementation objects [56]. However, even if attention is restricted to events, 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.

Any ``listener'' is only an approximation of an unobtainably ideal observer, and will have limitations in its ability to discriminate the occurrence of certain protocols. For example, it may be impossible in practice to obtain sufficient temporal granularity and synchronization of observations to recognize instances of, say, A B when event predicates in A and B are mapped to occurrences on different sides of the planet. (An intrusive alternative to detection is enforcement, using tools [10] that guarantee that certain messages obey certain orderings.)

Similar empirical challenges are encountered in relating the observation of a ``tapped'' message to a reception predicate for a particular role, detecting the creation of a new instance and its corresponding handle, as well as detecting different realizations of the same situation in multithreaded implementations.

Mappings of attributes remain the least automated aspect of tool development. Unless attribute functions are implemented by programmers, defined entirely via expressions on mapped observable event predicates, or are inferable via protocol rules, developers of tests and monitors must themselves implement all computable or approximable expressions of interest and implement them as program instrumentation. For example, the simplest possible testing tool would require implementations of boolean functions corresponding to each defined situation, along with history mechanisms recording event occurrences that are referenced in situation expressions. These functions may be invoked whenever a listener intercept notices an event that might make a situation of interest hold or stop holding. A more intelligent tool could infer the values of certain attributes without the need for instrumentation.

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: PSL: Protocols and Pragmatics Previous: Examples


Doug Lea@Sat Jun 3 07:20:05 EDT 1995