Jassda Trace Checker

The Trace Checker module of Jassda takes a specification describing all correct program behaviour. The check will test that the current program run is included in the set of allowed runs.

To specify the set of allowed runs the Trace Checker uses a CSP dialect, CSP_Jassda, that is tailored for Java programs. The main differences between standard CSP and CSP_Jassda are, that we use event sets instead of single events and that no interleaving is possible.

This page is work in progress. It is not complete, yet.

Events and Event Sets

Events of Java programs Jassda is interested in occur every time a method invocation begins or ends (either regularly or exceptionally), including the termination of an executed programm. Jassda uses the Java Debug Interface (JDI) to generate these events.
Events are characterized by certain inherent properties:

• name of class or interface
• method name
• thread information
• information about executing VM
• type of event
• ...

An eventset is, of course, a set of events. It therefore has to provide information about all of its belonging events. Eventsets are defined by:

• specification of properties (via key-value-pairs)
• binding of variables

The decision whether an event belongs to an eventset is made during runtime by a so-called handler-class.Jassda comes with a default handler-class: de.jassda.modules.trace.event.GenericSet.
It is also possible to use self-implemented handler-classes which are tailored to one's needs. In order to use them in a specification, a matching handler-class has to be given in the eventset's declaration.

Declaration of Event Sets

The are several ways to declare eventsets in specifications. The most straight forward method is the following declaration:

EventSetDeclaration ::= "eventset" <IDENTIFIER> "{" EventSetProperties "}"

This expression defines an eventset named by <IDENTIFIER> with the given properties. Properties are defined via the use of key-value-pairs describing all events contained in this eventset:

EventSetProperties ::= EventSetProperty ( "," EventSetProperty )*
EventSetProperty ::= <IDENTIFIER> "=" <STRING_LITERAL>

<IDENTIFIER> names a key, <STRING_LITERAL> the belonging value. All allowed keys are provided by the used handler-class. The default class de.jassda.modules.trace.event.GenericSet comes with several possible keys, e.g.:

• handler
• virutalmachine
• thread
• class
• method
• eventtype
• ...

Using the declaration as described above isn't the only possibility to define new eventset. Another method is the use of already declared eventsets:

EventSetDeclaration ::= "eventset" <IDENTIFIER> EventSetUnion

A union may be a single eventset, but it may also be put together from several intersections using the '+'-operator:

EventSetUnion ::= EventSetIntersection ( "+" EventSetIntersection )*

Intersections are declared using the '.'-operator:

EventSetIntersection ::= OutputEventSet ( "." OutputEventSet )*

Finally, a reference on an already declared eventset or a definition of a new eventset has to be provided:

OutputEventSet ::= PrimaryEventSet ( "!" PrimaryEventSet )*
PrimaryEventSet ::= EventReference | EventSetDefinition
EventSetDefinition ::= "{" EventSetProperties "}"

Note that it is possible to use combinations of references on eventsets and definitions of new eventsets.

Usage of variables

Besides the usage of the already explained eventsets, Jassda also allows the usage of variables. They may be used to store certain informations of events (e.g. informations about threads, classes or methods).
There are the following possibilities to use variables in specifications:

• variables combined with eventsets
• variables in quantified processes

Variables in combination with eventsets are only allowed in prefixing-processes:

InputEventSet ::= Union ( "?" Variable ":" Mapping )*
Variable ::= <IDENTIFIER>

If the prefixing-process accepts an event, the variable will store informations according to the mapping.

Mapping ::= "[" ( ClassName "," )? MappingComponent ( "," MappingComponent )* "]"
MappingComponent ::=( ArrayIdentifier | SimpleIdentifier ) [ "=" ( ArrayIdentifier | Name ) ]

The following excerpt from the CSP_Jassda-grammar describes the usage of variables in quantified processes (see also: chapter 4):

QuantifiedParallel ::= "||" Variable ":" Mapping "@" ParallelProcess
QuantifiedChoice ::= "[]" Variable ":" Mapping "@" ParallelProcess

Alphabets

With every process we associate an alphabet, i.e., a set of events that the process is interested in - now or in future. Every process should accept an event occuring during a program run if the process is active and the event is a member of the process' alphabet.

The alphabet of a process is calculated in two phases: in the first phase we collect all events that are mandatory to be part of the alphabet because of the structure of the process itself. We will call this the core alphabet of a process. In the second phase the alphabet is completed from the requirements of the process' context, thus forming the context alphabet.

Basic Processes

STOP

Process STOP does not accept any further event. This means that every event from the alphabet of the process is forbidden.

The core alphabet of process STOP is the empty set.

SKIP

Also, process SKIP does not accept any further event. But in contrast to STOP further events might be accepted if the SKIP process is part of a sequential composition

The core alphabet of process SKIP is the empty set.

Process Operators

Prefix ->

The prefix operator -> takes an event set on the left hand side and a process. A process "es -> P" will only accept events from the set "es" as first events. If such an event occured the process will accept the events of "P". Thus the prefix operator defines required sequences of events.

The core alphabet of a process "es -> P" is defined by the union of the events set "es" and the core alphabet of "P". Vice versa, the event set "es" must be a subset of the context alphabet of "P".

Choice []

The choice operator [] takes two processes. A process "P [] Q" will accept an event "e" if either "P" or "Q"accepts it. If "P" accepts the event let "R" be a process describing the events that are accepted by "P" afterwards. Let "S" be the process if "Q" accepts. Then after accepting "e" "P [] Q" will accept the events of "R" if only "P" accepts "e", will accept the events of "S" if only "Q" accepts "e" and will accept the events of "R [] S" if both accept "e".

The core alphabet of a process "P [] Q" is defined by the union of the core alphabets of "P" and "Q". Vice versa, the context alphabet of "P" and "Q" must be equal to the context alphabet of "P [] Q".

Parallel ||

The parallel operator || also takes two processes. A process "P || Q" will accept an event "e" if either "P" or "Q" accepts it. Additionally, if "e" is a member of both alphabets (a member of the intersection of "P"'s and "Q"'s alphabet), then "P" and "Q" must accept it (synchronisation), otherwise "P || Q" will reject it.

If "P" accepts the event let "R" be a process describing the events that are accepted by "P" afterwards. Let "S" be the process if "Q" accepts. Then "P || Q" will accept the events of "R || Q" if only "P" accepts "e", will accept the events of "P || S" if only "Q" accepts "e" and will accept the events of "R || S" if both accept "e", i.e., both processes synchronise on "e".

The core alphabet of a process "P || Q" is defined by the union of the core alphabets of "P" and "Q". Vice versa, the context alphabet of "P" and "Q" must be such that the union of both is equal to the context alphabet of "P || Q". Events, that are not part of one of the core alphabets of "P" or "Q" (but are in the context alphabet of "P || Q") are added to the context alphabet of both processes.

Interleaving |||

Like the parallel operator, the interleaving operator ||| takes two processes. A process "P ||| Q" will accept an event "e" if either "P" or "Q" or both accept it. Unlike the parallel composition, if "e" is a member of both alphabets (a member of the intersection of "P"'s and "Q"'s alphabet), either "P" or "Q" can accept it. The selection of the accepting process occurs non-deterministically. This non-determinism was realized as 'delayed selection': assume a process "P ||| Q". If "P" accepts the event "e" let "R" be a process describing the events that are accepted by "P" afterwards. Let "S" be the process if "Q" accepts. If "e" is in both processes' alphabets, both "P" and "Q" can accept "e". The resulting process will therefore be a choice consisting of the two possible follow-up processes: "(R ||| Q) [] (P ||| S)". This choice will be resolved as soon as possible: if for example an event "e2" is accepted only by "Q", the resulting process would be "R ||| S".

The core alphabet of a process "P ||| Q" is defined by the union of the core alphabets of "P" and "Q". Vice versa, the context alphabet of "P" and "Q" must be such that the union of both is equal to the context alphabet of "P ||| Q". Events, that are not part of one of the core alphabets of "P" or "Q" (but are in the context alphabet of "P ||| Q") are added to the context alphabet of both processes.

Also |+|

Like the parallel operator, the also operator |+| takes two processes. There are three different possibilities of an Also-process accepting an event "e": If "P" accepts "e" and "Q" rejects it, then "P |+| Q" will accept the event with the follow-up process "R" of "P". Similarly, if "Q" accepts the event and "P" rejects it, then "P |+| Q" will accept "e" with the follow-up process "S" of "Q". And finally, if both "P" and "Q" accept "e", then "P |+| Q" will accept the event with the follow-up process "R |+| S". Note the similarity with the Interleaving-operator in the first two cases, and the similiarity with the Parallel-operator if both "P" and "Q" accept an event at the same time. "P |+| Q" can reject an event "e" only if both subprocesses "P" and "Q" reject "e".

The core alphabet of a process "P |+| Q" is defined by the union of the core alphabets of "P" and "Q". Vice versa, the context alphabet of "P" and "Q" must be such that the union of both is equal to the context alphabet of "P |+| Q". Events, that are not part of one of the core alphabets of "P" or "Q" (but are in the context alphabet of "P |+| Q") are added to the context alphabet of both processes.