The Implementation of JavaTriveni

We have implemented Triveni in Java as a class library. The design of the JavaTriveni implementation and the underlying algorithms are described in [CJJ⁺98]. The relationship between class names and event labels in Triveni must currently be established by the application programmer and is not currently enforced by the system.

Here, we briefly sketch the architecture of a Triveni process, referring the reader to [CJJ⁺98] for details. The implementation of a JavaTriveni process P comprises of a controller C_P, which is a deterministic state machine, and a multiset of concurrent communicating activities ( $\{A_{P,1},\ldots,A_{P,n}\}$), possibly implemented in the host language Java. In particular, event emissions are realized as activities. Every transition in the state machine C_P is labeled with an event name and a set of side-effects that will occur when this transition is taken - these side effects can include control operations on activities via the Controllable interface, such as start(), suspend(), resume(), and stop(). A given transition labeled e is triggered upon receipt of an event with label e if the current state of the state machine is the source state of the transition. C_P also controls all communication between its activities -- each activity A_P,i emits events to C_P, which may forward it back to one or more selected activities A_P,j. The implementations of all Triveni combinators operate on such structures and yield such structures.

Our JavaTriveni implementation includes a non-intrusive form of instrumentation for testing and debugging in the flavor of assert statements in traditional languages. In particular, system specifications can be expressed as safety properties; informally, these properties stipulate that ``something bad never happens.'' Temporal logic is a well-known formalism for specifying safety properties, and our specification language is based on its propositional linear-time variant [MP92]. This notation provides a straightforward means of expressing conditions on sequences of events.

Our implementation uses the following fact about safety properties: for any safety property, there exists a finite-state machine whose language is the set of all possible (finite) executions that violate the property. From the given property, our implementation automatically generates a JavaTriveni process, which encodes this finite-state machine. This process is composed in parallel with the process that is being monitored. If the specified property is violated at any point during an execution of the system, the above JavaTriveni process generates a special event, and the assertion fails. The user has the option to abort the application, ignore the failed assertion, or ask the system to report entire test traces.