This document is also available in non-normative PDF version.
Copyright © 2004 DERI ®, All Rights Reserved. DERI liability, trademark, document use, and software licensing rules apply.
In this deliverable we define the execution semantics of the Web Services Execution Environment. Accommodating for readers unfamiliar with the term execution semantics, we first describe what is meant by this concept. Next we explore different modelling techniques for defining execution semantics in existing literature and choose an appropriate modelling technique. Using this technique we define the execution semantics of the Web Services Execution Semantics, so that its operational behaviour is formally -unambiguously- specified. [note: this deliverable is in very preliminary draft version, so the following text is to be read as guideline of further work; this will not be the final text].
Execution semantics (or operational semantics) is a formal definition of the operational behaviour of a (software) system. It describes -in a formal language- how the system behaves. Because the meaning of the system (to the outside world) consists of its behaviour, this formal definition is called execution semantics.
A formal definition is a specification in a formal language, i.e. a language for which a mapping to a mathematical model -in which the grounding axioms, the concepts and the relations between them are described- is defined. A mathematical model has a (possibly many) interpretation that describe how statements in the model should be interpreted (with respect to the real-world domain).
In a model certain statements can be deduced from other statements. This is called logical inference. A model is sound if only true statements can be deduced, i.e. that a deduced statement is really a logical consequence of the existing statements, which means that no false statements can be deduced. A model is complete if every logical consequence can be deduced in the model. So, the completeness property certifies that the model is powerful enough to deduce all that could be deduced logically while the soundness property certifies that no false statements could be deduced.
A formal definition should be sound and complete with respect to the modelled behaviour. If not, it is useless for reasoning because it doesn't represent the real-world behaviour correctly: it would for instance be possible to deduce statements in the model that are not true in the real-world.
A sound and complete formal definition makes it possible to reason about statements in the language, using proved logical entailments. In that way the behaviour of the system can be checked before (or without) implementing it. If the model is sound and complete it would be possible the prove statements about the system, for instance that there are no unreachable states (i.e., that there are no parts of the system that are not used), or that the system will reach a terminating state eventually (i.e., that there is no livelock).
For modelling the execution semantics of a software system different modelling techniques are available; choosing a certain technique can be done based on several criteria. The most important criterium is that there should exist a proof of the soundness and completeness of the technique, as stated above. Secondly, depending on the specific system to be modelled, criteria could include the ease of checking the model, the possibility to simulate model, the possibility to model concurrent systems, and so on.
To choose an appropriate method for defining the execution semantics, first a literature-based comparison of different modelling techniques for execution semantics will be performed. After that, we will choose a technique to model the Web Services Execution Environment, and using that technique define a formal model that describes the complete behaviour of the Execution Environment.
As a small example of a execution semantics of a specific system, a Petri-net model is shown below, of a machine that processes (some) jobs. The modelled system is thus not a software system, but a real-world machine. However, the modelling technique is indifferent to this (artificial) difference; below another example is shown, that deals with software systems.
A Petri-net is a directed bipartite graph, consisting of a set of places (that could be used to model states or events) and transitions. Places can only be connected to transitions, and vice versa. A transition has one or more input places, and one or more output places. A place can contain one or more tokens. If a place contains at least one token, it is enabled. A transition can fire if all his input places are enabled, i.e. if all his input places contain at least one token. Upon firing, a transition consumes a token from every input place, and produces a token in every output place. A Petri-net model can be used (for instance) to model states and state-transitions of a system.
The example shown models a machine that has an input-queue, representing jobs to be processed (this is an interpretation of course, and does not affect the model), and an output queue, representing jobs that have been processed. The machine itself has two states, it is either 'busy' or 'free'. The 'start_job' transition can only fire if the machine is in the state 'free', and if there are any jobs in the 'in_queue'.
Using Petri-net, the behaviour of the modelled system can be simulated very easily (and analysed mathematically, which is not shown here). In the figure below, the modelled machine is simulated; it has currently three jobs that should be processed, and the machine is 'free'.
The transition 'start_job' is enabled, since all its input places contain one or more tokens. Upon firing, this transition consumes a token from both these places, and produces one token in the 'machine_busy' place. This can be seen in the second 'snapshot', shown below:
Now the transition 'finish_job' is enabled, and upon firing it will consume the token in the 'busy' place, and place a token in the 'free' place, and in the 'out_queue', as is shown again below:
This process will repeat itself until there are no more jobs to be processed in the in_queue. Several characteristics of the system can be deduced from this model, for instance that no job will circulate in the system in an infinite loop (i.e., there is no livelockness), or that no place in the system is unreachable (i.e., no dead places). These analyses are mathematical in nature and can be founded in standard Petri-net literature.
This Petri-net technique could be extended with several concepts, to model systems in a more convenient way; it is important to notice that the expressive power of extended Petri-net is equal to that of simple Petri-nets as described here. Some often used extensions are coloured Petri-nets, hierarchical Petri-nets and timed Petri-nets.
To show that Petri-nets can be used to model the execution semantics of a software system and also to show that these models are often not trivial, another example is shown here. The Petri-net models a virtual network of communicating peer-to-peer agents. These agents act on behalf of a user, and are responsible for maintaining the user profiles of all members of this virtual network, as well as for maintaining the online state of these members. In order to do so, all agents communicate with one another to inform and enquire about changes in the virtual network.
The model is shown below, and is not very readable because no use has been made of hierarchical Petri-nets. This should be done in order to break down the information into human-manageable modules. However, this model (and the possibility of simulation) has already proven useful in the design of these agents, both in explicitly stating design ideas and thereby stimulating early discussion of essential elements, and in finding design flaws leading to deadlocks and livelocks.
