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|
E
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.
Details
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|
S
An example is the following method.
receiveInput(b: Bool)(r: Object)
| |
if b then
p1 ? input(r)
else
p2 ? input(r)
fi
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.
Figure 1. Example of graphically denoting a behaviour specification.