Parallel Object-Oriented Specification Language

The Parallel Object-Oriented Specification Language (POOSL) is a very expressive language to model concurrent hardware/software systems. POOSL has a small set of powerful primitives and it has an unambiguous formal semantics in terms of mathematical axioms and rules. POOSL models can be simulated with the Rotalumis simulator. There is an Eclipse-based tool for editing and debugging POOSL models PooslIDE (and the older, no longer developed SHESim tool). An experimental POOSL unit testing plug-in is available for the Eclipse-based editor.

The formal semantics of POOSL forms the basis of Markov-chain based performance analysis techniques and run-time model checking techniques for Formal Verification of correctness properties. It furthermore serves as a basis for a software synthesis technique that preserves timing properties.

The language is structured into three layers the first layer captures passive data objects. The second layer active process objects and the third describes system structure and architecture. Below we present the syntax of Data, Process and Architecture layers of POOSL and we briefly discuss a few aspects of the meaning (semantics).

In case you want to refer to POOSL, you can use the following reference:

B.D. Theelen, O. Florescu, M.C.W. Geilen, J. Huang, P.H.A. van der Putten and J.P.M. Voeten, Software/Hardware Engineering with the Parallel Object-Oriented Specification Language. In: Proceedings of MEMOCODE’07, pp. 139-148, 2007

Data Layer

The data layer is a probabilistic version of traditional imperative object-oriented programming languages and supports the object-oriented principles of encapsulation, single inheritance (including method overriding) and polymorphism. All data in a POOSL models is represented by data objects, which are instances of data classes. A data class has a name, a (single) inheritance relation, instance variables and instance methods. Every data class directly or indirectly inherits from the data class called Object, which is the only class that does not inherit from any other class. The instance variables specify the attributes of a data object. A data class inherits all instance variables of its super class and may add variables of its own. The behaviour of data is sequential and defined by its instance methods or (data) methods. Data classes inherit all methods from their super classes and may redefine or add methods. Data objects may receive a messages from data objects or from processes, which automatically leads to the execution of a method with the same name as the message. As usual, this may in turn lead to other data methods of the object or of other objects being called recursively. Upon completion of the method, a result in the form of a reference to a data object is always returned. This may be the receiver of the message, but also any other data object as specified by the method that was executed. In summary, data objects are very similar to objects in traditional imperative object-oriented programming languages such as Java or C++.

Data methods

Data methods are defined according to the following form:

m(p1: DC1, ..., pi: DCi) : DCr
|l1: DCl1, ..., lk: Dlk|

An example is the following method.

vectorLength(x: Real, y: Real) : Real
| dsqr: Real |
dsqr := x sqr() + y sqr();
return dsqr sqrt()

In general, m is the method name (vectorLength in the example) and DCr (Real) is a data class name that denotes the type of the object returned by the method (see below for a short note on the type system of POOSL). The lists p1: DC1, ..., pi: DCi defines the formal arguments of the method. When the method is called, values (references to data objects) need to be supplied, which will be bound to local variables with the corresponding names (p1, pi) before the method starts. DC1, DCi specify the types of the parameters. l1: DCl1, ..., lk: DClk, written between vertical bars denote similarly the other local variables of the method. The body of a data method is a data expression E. Note that this expression may itself be composed as a sequence of smaller expressions as in the example method.

Primitie and Native Data Classes

Some data classes are primitive. This means that they are defined by the semantics of the language. Models can add non-primitive data classes of their own. Primitive data classes have primitive methods, the behaviour of these methods is defined by the semantics, but models can add their own methods, as described above, also to primitive classes.

Specific tools may also offer native data classes with native methods. These are defined by the tool implementation, not the formal semantics. They are used, for instance, for I/O purposes.

The primitive classes are: data class Object (the root of the inheritance hierarchy), with primitive methods like =, !=, ==, deepCopy and shallowCopy (which can therefore be used on any data object) and the data classes Boolean, Integer, Real, Char and Nil. Data class Boolean has exactly two instances, called true and false. Data classes Integer and Real have exactly one instance for each numerical value that they can represent, so there is exactly one Integer object 1(!). Instances of data class Char represent strings and the primitive methods of this class reflect standard operations on strings. Data class Nil has only a single instance, nil.

Native data classes in the POOSL tools are String, Array, FileIn, FileOut and RandomGenerator. A String represents a string of (extended ASCII) characters as usual. An object of class Array holds an array of data objects. FileIn and FileOut manage file I/O. Instances of RandomGenerator represent a pseudo random number generator.

Data Expressions

E ::= c                          literal
   |  x                          variable
   |  self                       reference self
   |  new(D)                     data object creation
   |  currentTime                current model time
   |  x := E                     assignment
   |  E1; E2                     sequential composition
   |  E m(E1, ..., Ei)           data method call
   |  self ^m(E1, ..., Ei)       superclass data method call
   |  if Ec then E1 else E2 fi   choice
   |  while Ec do E od           loop
   |  return E                   annotation of an intended return value in a method

Table 1. Expressions.

The behaviour of ordinary, non-primitive data methods is specified by expressions. Table 1 summarises the syntax for the most relevant forms of expressions. Literal c refers to an instance of one of the data class Boolean, Integer, Real, Char, String or Nil that has an explicit syntactic form. Examples are Boolean true, Real 3.8, Char 'z' and String "POOSL". The expression x denotes a (instance or local) variable name and it evaluates to the object referred to by the variable x. The keyword self evaluates to the data object that is evaluating the expression. Evaluation of new(D) results in the creation of a new instance of data class D and evaluates to a reference to that new object. Note that instances of Boolean, Integer, Real and Char are immutable and will always keep the same value. Expression currentTime evaluates to a numerical values that denotes the current model time. It can only be used in the context of processes. Expression x := E denotes the assignment of the value to which E evaluates to variable x. As an expression by itself, it evaluates to the same value. It is therefore possible to write, for instance, x := y := z := 0. Sequential composition of expressions is denoted using a semicolon. Be aware that the semicolon is used only between expression, not, as in many other languages, at the end of every expression. In particular, the last expression is not followed by a semicolon. Parenthesis can be used to group expressions.

The next expression in table 1 is the data method call E m(E1, ..., Ei). Evaluation results in the invocation of method m for the object to which expression E evaluates. The expressions E and E1, …, Ei are evaluated (from left to right) and passed as parameters to the method. If the data class of the object evaluating the expression redefines or overrides a method m of its superclass by defining a method with the same name m and the same number of parameters, then the expression self ^m(E1, ..., Ei) invokes the inherited method m as defined in the superclass.

Expression if Ec then E1 else E2 fi evaluates to the result of expression E1 in case the condition Ec evaluates to true and E2 if it evaluates to false. The loop while Ec do E od, repeatedly evaluates expression E as long as condition Ec evaluates to true and ends when Ec evaluates to false the expression itself always evaluates to nil. The expression return E is fully equivalent to the expression E in any context where it is allowed to be used (only in data methods). It can be used to emphasize the intended result to be returned after completion of the method.

Type System

POOSL includes a type system for data objects. The extent to which types are checked, statically or dynamically, is left to the specific tools. In terms of the semantics of the language, the type system is not used. The type system is simply defined as follows. With every data class DC, a type is associated that includes all instances of class D or any sub class of D and every type includes the object nil (the single instance of the data class Nil, which is used to initialise all fresh variables).

Memory Management

In POOSL it is not possible to explicitly destroy objects. In the formal semantics, objects that are created remain in existence forever. The tools handle this by on automatic storage reclamation, Garbage Collection, for objects that can no longer be accessed by any active objects in the model.


The native class Random Generator has a primitive method random that returns a Real according to a uniform distribution (0, 1), while primitive method randomInt, which has an Integer parameter p, returns an Integer according to a uniform distribution [0, p). The primitive method seed initialises the initial value (seed) of the random number generator used for implementing random and randomInt. Primitive method randomiseSeed initialises the seed in an arbitrary way based on the real time at which randomiseSeed is evaluated. To obtain random numbers according to various other distributions, a library of Distribution Classes has been predefined for POOSL and is available here.

Here is an example of a complete data class definition.

Process Layer

Process objects or processes, in short, distinguish themselves from data objects by the fact that they are static, active and concurrent objects in a POOSL model. The behaviour of processes is defined by process classes. A process class has a name, instantiation parameters, instance variables, ports, a message interface, instance methods, an initial method call and an (optional, single) inheritance relation.

The instantiation parameters and instance variables are the attributes of a process object. The instantiation parameters are given values when the process is instantiated. This allows their behaviour to be parameterised.A typical example is to provide different instances of the same class with a unique identifier. Processes can communicate via their ports. The message interface lists the signatures of all possible messages that the process may use and includes for each message the name of the port, the symbol ! or ? for send and receive messages respectively, the message name and a (possibly empty) list of types of the message parameters.

The behaviour of processes is defined by the instance methods or (process) methods of the process class. Methods may be called with formal input parameters (like data methods) and may, in contrast to data methods, return multiple results through output parameters. The startup behaviour of a process is defined by the initial method call. In case an process class inherits from another process class, it inherits the instantiation parameters, instance variables, port interface and message interface as well as all the methods of its superclass.

Process Methods

The behaviour of a process method is specified using the following syntax:

m(p1: Dp1, ..., pi: Dpi)(r1: Dr1, ..., rj: Drj)
|l1: Dl1, ..., lk: Dlk|

An example is the following method.

receiveInput(b: Bool)(r: Object)
| |
if b then
	p1 ? input(r)
	p2 ? input(r)

m is the method name and declarations p1: Dp1, ... pi: Dpi, r1: Dr1, ... rj: Drj and l1: Dl1, ..., lk: Dlk denote the input parameters, output parameters and local variables, respectively for method m. Similarly to data method, they are defined with names and types. The body of m is defined with a statement S. The syntax for statements is shown in table 2.

Process Statements

S ::=   E                           expression
   |    m(E1, ..., Ei)(v1, ..., vj) process method call
   |    par S1 and ... and Sn rap   parallel composition
   |    S1; S2                      sequential composition
   |    p!m(E1, ..., Ei){E}         message send
   |    p?m(v1, ..., vi | Ec){E}    (conditional) message reception
   |    sel S1 or ... or Sn les     non-determinis tric selection
   |    [Ec]S                       guarded statement
   |    interrupt S1 with S2        interrupt
   |    abort S1 with S2            abort
   |    delay E                     time delay
   |    if Ec then S1 else S2 fi    choice
   |    while Ec do S od            loop
   |    skip                        empty behaviour

Table 2. Statements.

Most data expressions of table 1 are also valid statements (exceptions are expressions using self and return E). It is possible to surround data expression with curly braces to enforce atomic (indivisible) execution of the expression. This may be needed, because processes execute concurrently. The statement m(E1, ..., Ei)(v1, ..., vj) makes that method m is called after expressions E1, …, Ei are evaluated from left to right and bound to the input parameters of m. After the execution of m, results are returned by binding the returned objects to variables v1, …, vj. Methods without output parameters may be called in a tail-recursive manner.

The par statement for parallel composition denotes the concurrent, non-deterministically interleaved execution of statements S1, …, Sn. This allows asynchronous concurrency within processes besides concurrency among processes. Sequential composition of statements is denoted using a semicolon. Similar as for expressions, sequentially composed statements can be grouped using the optional parentheses.

The message send statement p!m(E1, ..., Ei){E} leads to the synchronous sending of message m to port p. It only happens when a matching message receive statement is executed by another process connected to the same channel to which the port connects. Parameters E1, …, Ei are evaluated from left to right and (recursive, ‘deep’) copies of the resulting data objects are bound to the parameters of the corresponding receive statement. The send statement can optionally be followed by a data expression between curly braces. In that case the expressionb is evaluated, atomically, immediately after the message is sent. The complementary message receive statement p?m(v1, ..., vi | Ec){E} synchronously receives message m on port p. The parameters accompanying the received message are bound to variables v1, …, vi. The synchronisation only occurs if the message names match, the number of parameters are equal and the optional reception condition Ec (which may depend on the data objects that are being received!) evaluates to true. Also the receive statement may be followed by an atomically evaluated expression.

The select statement sel S1 or ... or Sn les for non-deterministic selection executes one of its constituent statements S1, …, Sn that is enables to execute an action. A time delay postpones the decision. The guarded statemtn [Ec] S inhibits the execution of S as long as the condition expression Ec evaluates to false.

The interrupt statement interrupt S1 with S2 executes S1 until S2 starts execution. At that time, S1 is suspended until S2 completes. Then S1 resumes, but can be interrupted by S2 again. When both S1 can progress and S2 can start the decision is made non-deterministically. The statement abort S1 with S2 behaves similarly, but S1 is terminated when S2 starts executing.

The statement delay E delays further execution for a duration of simulation time equal to the result of evaluating E. It is the only statement to express quantitative timing behaviour. It can be combined with other statements to realise more intricate timing behaviour like time-outs or watchdogs. The time domain of a model can be discrete (when delays are integer or dense when delays use Reals.

The if an while statements behave like their data expression counterppoarts. The skip statement performs an (internal) action without any side effect. It is meaningful in combination with other statements.

Here is an example of a complete process class definition.

Architecture Layer

The architecture layer allows one to hierarchically build a structure of process objects connected with channels, using clusters. Clusters are defined by cluster classes.

A cluster class has a name, instantiation parameters, ports, a message interface and a behaviour specification. The instantiation parameters are the attributes that can be used to parameterise a cluster, similar to the instantiation parameters of process classes. The ports and message interface define how a cluster may communicate to the outside. They are defined in the same way as for process classes.

The behaviour specification defines what instances of process and clusters exist in the cluster instantiated from the class and how they are connected by channels. Channels may connect only instances inside the cluster, but channels may also connect to the outside ports of the cluster. The specification also provides expressions for all instantiation parameters of the instances inside the clusters. Those expressions can in turn refer to the instantiation parameters of the cluster class being defined. It is important to be aware that the language semantics defines that two ports *of the same instance (cluster or process) that are externally connected by a channel do not allow a message passing synchronization to occur. This is only possible between ports from different instances, or between an instance and an external port.

The final part of the architecture layer is the specification of the top-level diagram or system specification of a model. The system specification defines the processes and clusters that are instantiated in the actual model and how they are interconnected by channels. At this level, there are no external ports.

figure 1 shows the behaviour specification of a cluster class C with parameters p1, …, pn, which encapsulates instances A and B of process classes P1 and P2. Their parameters are initialised by expressions PE1, …, PEi and PE1, …, PEj respectively, which may depend on p1, …, pn. Processes A and B may communicate via ports a and b respectively over channel ch, which is also connected to port c of C.

Example instance structure

Figure 1. Example of graphically denoting a behaviour specification.