Abstract: In this study it is proposed a formal semantics for Basic LOTOS (Language Of Temporal Ordering Specification). The subset of LOTOS, where processes interact with each other by pure synchronizations, without exchanging values. In basic LOTOS the expressiveness of all the LOTOS process constructors (operators) can be appreciated without being distracted by interprocess value communication. LOTOS is an FDT generally applicable to distributed, concurrent information processing systems. During the last decade, a lot of works have been devoted to compilation and verification of LOTOS specifications. While using extended Petri nets as tool for compile a subset of LOTOS has already been pointed out. In this research it is proposed to extensively make use of a specific kind of high level Petri nets: the M-nets. Such nets, allowing for compositionality, appear particularly well-suited to give a formal semantics for basic LOTOS.
INTRODUCTION
LOTOS (Garavel, 1990) is one of the Formal Description Techniques FDT developed within ISO for the formal specification of open distributed systems. In LOTOS a distributed, concurrent system is seen as a process, possibly consisting of several sub-processes. A LOTOS specification describes a system via a hierarchy of process definitions. A process is an entity able to perform internal, unobservable actions and to interact with other processes, which form its environment. Basic LOTOS is a simplified version of the language employing a finite alphabet of observable actions. This is so because observable actions in basic LOTOS are identified only by the name of the gate where they are offered and LOTOS specifications can only have a finite number of gates.
The M-nets calculus (Best et al., 1995, 1999) defined as the high level or coloured version of the Petri Box Calculus (PBC), is widely accepted to give semantics to concurrent systems and programming languages like B(PN)2 and SDL, cf. (Lilius and Pelz, 1996; Fleischhack and Grahlman, 1997; Klaudel and Reamann, 1995; Best et al., 1999). The most original aspect of M-nets is their full compositionality thanks to their interfaces and a set of various net operations defined semantics for them. In fact, M-nets constitute like PBC a net algebra. Their interest is augmented by the ability to use in practice an associated tool PEP (Programming Environment based on Petri nets) (Grahlman, 1997), which also offers various implemented verification and analysis methods. Whenever the system to be modeled consists of a lot of distinct conceptual parts, which need to be combined or coordinated in a non trivial way, a very modular and compositional proceeding is necessary to be able to control the correctness of modeling (BuiThanh and Klaudel, 2003, 2004). M-nets just offer these features. We have chosen to translate basic LOTOS specifications into the algebra of modular high-level Petri nets: the M-nets (Best et al., 1995, 1999; Klaudel, 1995). Due to the rich set of composition and communication operators we are able to define a semantic operator on M-nets for each syntactic operator of basic LOTOS. Using our approach a property of a basic LOTOS specification is checked as follows:
| • | The M-net semantics of the basic LOTOS specification is calculated |
| • | The M-net is unfolded into a Petri box (a special low-level net) |
| • | The basic LOTOS property is transformed into a net property |
| • | The net property is checked against the Petri box |
| • | The result is transformed back to the basic LOTOS level |
BASIC LOTOS SPECIFICATION
Systems and their components are represented in LOTOS by processes. A specification is the process that represents the whole system being specified. A process displays an observable behaviour to its environment in term of permitted sequences of observable actions (Garavel, 1990). A process appears as a black box to its environment since the environment has no information about its internal structure and mechanisms. Processes may have a local definitions (after the keyword where) in which other processes can be defined. LOTOS has scoping rules similar to block-structured programming language. The structure of basic LOTOS specification is:
| specification | spec-name [gate list]: functionality behaviour expression |
| where | |
| process definitions | |
| endspec |
where gate list is a finite alphabet of gate names (or observable actions). A behaviour expression is built by applying an operator (e.g., `[]`) to other behaviour expressions. A behaviour expression may also include instantiations of other processes whose definitions are provided in the where clause following the expression. The complete list of basic LOTOS behaviour expressions is given in Table 1, which includes all basic LOTOS operators Symbols B, B1, B2 stand any behaviour expression; G, G1, G2,…,Gn are elements of a finite alphabet gate list.
Remark: As we will see farther, the parallel operator `||` take an important part in the M-nets algebra; thus, in order to avoid confusion we reserve this notation for the composition of M-nets. In the sequel, for LOTOS, the notation for the operator of full synchronization will be |[G+]| instead of || where G+ is the set of all gates which are defined in both behaviours or both processes.
M-nets: The M-nets algebra was introduced in (Best et al., 1995, 1999) as an abstract and flexible metalanguage for the definition of semantics of concurrent programming languages. These allow (as usually composition operators in process algebras do) the compositional construction of complex nets from simple ones, thereby satisfying various algebraic properties. the main difference between M-nets and coloured nets is that M-nets carry additional information on their places and transitions to support composition operations. Besides annotations on places (set of allowed tokens), arcs (multisets of variables and transitions (occurrence conditions), M-nets have, additionally, labels on places and labels on transitions. The labels on transitions denote communication capabilities similar to action symbols in a CCS term, respectively indicate their hierarchical nature. The labels on places denote their status as entry (part of the initial marking), exit (part of the final marking) or internal (othrewise).
| Table 1: | Syntax of behaviour expressions in basic LOTOS |
internal (otherwise). Thus, every place and transition
of an M-net carries an inscription of the form inscription = (label
| annotation). |
|
Thus, every place and transition of an M-net carries an inscription of the form inscription = (label | annotation ).
Auxiliary definitions: Let Val be a fixed and suitably large set
of values, Var, resp. X sets of variables, resp. hierarchical variables,
the latter ones being capital letters and Par a set of parameters. We
assume the existence of a fixed but sufficiently large set A of parametrised
action symbols. Each action A ε A is assumed to have an arity
ar(A) which is a natural number describing the number of its parameters.
The elements of A are grouped into pairwise conjugates by the bijections:
A → A, called conjugation, satisfying:
It is also assumed the existence of a fixed but sufficiently large set G of action gate symbols without conjugation. Each action gate symbol G ε G is assumed to have an arbitrary arity ar(G) An action term is, by definition, a construct A(A(τ1,…,τar(a), G[G1,…,Gar(A)] where A ε A and τj ε Var ∪ val for 1 ≤I≤ar(A); G ε G and Gi ε gatelist for 1≤i≤ar(G).
Definition of M-nets: An M-net is a triple (P, T, λ) such that P is a set of places, T a set of transitions with P ∩ T = Ø, λ is an inscription function with domain P ∪ (P xT) ∪ (TxP) ∪ T, such that:
| • | For every place p ε P λ(p) (αp, βp), where α(p) ε {a,i,x} is called the label or status of p and β(p), the type of p, is a nonempty set of values from Val. |
| • | For every transition t ε T λ(t) is a pair (αt, βt) where αt, the label of t, is a finite multiset of action terms (t will then be called a communication transition), or a hierarchical action symbol, i.e., α (t) ε X, (t will then be called a hierarchical transition); β(t), the gard of t, is a multiset of terms over Val and Var. |
| • | For every arc (p,t) ε (PxT), λ(p,t) is a finite multiset of variables from Var and values respecting the type of the adjacent place p, (analogous for arcs (t, p) ε (TxP)); the meaning of λ(p,t) = Ø is that there is no arc leading from p to t (Benzaken et al., 1998). |
Operations on M-nets: The composition operators on M-nets as defined in (Best et al., 1995; Klaudel, 1995) are two different kinds: those concerning place interfaces and thus the flow control (which comprise sequential composition ;, choice [], parallel composition || and iteration *) and those concerning transition interfaces and thus capabilities for communication comprising synchronization and restriction.
The intuitive idea behind the synchronisation operation of an M-net N consists of a conglomeration of certain basic synchronisations over actions terms pairs (A(.,.) and et al., 1999). The operation will be defined as follows: N sy A, where N = (P,T,λ) is a given M-net and A is a given action symbol. The communication is performed by a most general unifier which renames the variables in the action terms appropriately (Klaudel, 1995). The restriction operation N rs A removes from N all transitions that mention either A or
Scoping is a mixed operation, accepting an M-net and a set of communication action symbols; it is defined by the synchronisation followed by the restriction of the net over the set of action symbols: N` = (N sy A) rs A. This scoping mechanism is used for block structuring.
M-net model extensions: In order to adapt the M-net model for a basic LOTOS compositional semantics, the operations on M-nets must be extended to some other operators such that:
| • | The M-net refinement (Reimann et al., 2003; Devillers
et al., 2003; Klaudel and Riemann, 1998): N[Xi ←
Ni|i ε I] allowing a hierarchical construction
of M-net, means N where all Xi-labeled (hierarchical) |
transitions are refined into (i.e., replaced by a copy of) Ni,
for each i in the indexing set I. However, general refinement (Riemann
et al., 2003) is not sufficient for our approach; in fact,
knowing that a LOTOS system is described via a hierarchy of process
definitions it must has a possibility to distinguish different instantiations
of a process definitions and their behaviours. In order to satisfy
this requirement, it is used the general parametrised refinement concept
(Devillers et al., 2003). The parameter mechanism is the mean
by which a refining net interact with the area of the refined transition. In this way, a formal parameter is add to hierarchical transition which deals with the concrete parameters of the call and return transitions labels that we see later. |
| • | The synchronization-lotos (Mekki, 2000) sylotos is defined such that: Let two M-nets N1 = (P1,T1,λ1) and N2 = (P2,T2,λ2) and let G an action gate symbol. (N1||N2)sylotos = (P,Tλ)
where: |
| • | The relabelling function (Mekki, 2000): ∏pgatelist which is applied to an M-net N, is parametrised with a name of process definition (P) and a list of gate names (gate-list). It does the following substitution for each gate name Gi ε gate-list in N. |
Semantics of a basic LOTOS specification: A semantics of basic LOTOS specification will be defined associating one M-net to each process definition (avowed in the where clause) its behaviour expression.
The initialization and clearing of each process definition The M-net of the last two kinds have to be composed sequentially with each other to enable later scoping over (created and terminated) processes. Finally, all these M-nets are put in parallel and the synchronization and restriction ovet all action names in the process definitions will insure the scoping. Thus, we get above global semantic formula:
M–net(bloc) = [M–net(process definitions)
||I (processes); M–net(behaviour expression;
ΓT(processes))] sy Γ(processes) rs Γ (process)
Withwhere, γnI (processes) and γnT (processes) are the auxiliary M-nets for initialization and termination of scoping.
In the sequel, the other M-nets appearing in the above global semantic formula will be precisely defined as well as the considered sets of action symbols.
Semantics of process definition: A process definition is similar to a procedure declaration in a programming language like Pascal. Let us first examine a single instantiation of a process.
| Fig. 1: | Semantic components of process definition Pj |
It is easy that it consists of a call transition,
a return transition and a body. The call transition is labeled with
In the sequel, it is supposed that the set ID(P) ⊆ Val of instantiation identifiers is given. As mentioned in the introduction, generally a specification LOTOS is a hierarchy of processes. Therefore, it may has overlapping process definitions. Hence, in order to deal with process definition formally, we will denote by Pj a process definition identifier at the jth level of overlap (with 1≤#m where m is the maximal depth of overlap).
The box M-net (procdef) of a process definition declared at the level of overlap depth j is obtained by successive refinements in the operator M-net.
NI NIj (id1:Id(P),...,idj–1:Id(P)) of semantic components of Pj where:
Nij (id1:Id(P),...,idj–1:Id(P)) in charge for the management of instanciations Pj;
In the box
must be renamed in list of effective gates belonging instanciation Pcall M-net.
This renaming is obtained using the function Pipgate–list.
Finally, after refinement in
M-net(procdef} is obtained from the following expression:
In a basic LOTOS specification or process, the declaration semantics of many process definitions with same overlap level is given by the following formula:
M-net(process definitions) = ∏kn=1Pn
and the action symbols for scoping are:
where:
with
and
Behaviour expression M-net: An essential component of a specification is its behaviour expression where the observable and intern behaviours are defined. It is the specification behaviour obtained by combination of the behaviour operators (sequential composition, parallel composition, ….
In the sequel, the M-nets semantics of each operator (Table 1) is given.
Inaction specified by stop, models a situation in which a process is unable to interact with its environment. Inaction can be used to describe deadlock (Fig. 2).
Successful termination: In LOTOS exit is a nullary operator. It is equivalent to the following behaviour: δ; stop, this sequential composition is an interaction with the special succefull termination gate δ, which ever appears explicitly in LOTOS program, followed by a stop operator Fig. 2.
Action prefix:: The semantics of action prefix behaviour expression B is:
M-net (G ; B) = M-net(G); M-net(B) where M-net(G) is given in Fig. 2.
Choice: M-net(B1[]B2 = M-net (B1) M-net(B2)
Parallel composition: LOTOS has three kinds of parallel operators (Table 1):
| • | General case B1|[{G1,...G2}∪{δ}]|B2 where {G1,...,Gm} a set of user-defined gates called synchronization gates of B1 and B2 |
| • | Pure interleaving B1|[G]|B2 when the set of synchronization gates is only δ. |
| • | Full synchronization B1|[G]|B2 when the set of synchronization gates is the set of all gates appearing in both behaviour expressions including δ. The M-nets semantics of parallel operators is carried out in two stages: Concurrency is expressed applying the parallel operator of M-nets algebra ( || ). |
| Fig. 2: | M-netstop , M-netexit and M-net of action over the gate G |
Synchronization and communication LOTOS are expressed by coupling of all the committed transitions in a same event. Two transitions t1 and t2 belonging respectively to M-nets B1 and B2 must synchronize through sylotos if they have in their respective labels the same action gate symbol belonging to the set of synchronization gates of specified operator, either [G1,...,G2] for the first case and [G] for the second. Thus, the semantics of this three operators is:
with [G1,...,Gn] = [gatelist]
Sequential composition:
Hiding: The operator hide … in allows one to transform some observable actions of a process into unobservable ones. The M-nets semantics for the hiding operator consist of a renaming of all hiden gates by i (unobservable action) (Best et al., 1999) over which no more interactions are possible.
M–net(hide G1,...,Gr in B) = M–net(B) where G1,...,Gr are renamed by i.
Disabling: B1[>B2. In almost any OSI connection oriented protocol or service.
| Fig. 3: | M-net(TAbort) and M-net(Abort) |
| Fig. 4: | Process instantiation: Pcall |
It is the case that the normal course of action can be disrupted at any point in time by events signaling disconnection or abortion of a connection. This has led to the definition in basic LOTOS of an application generated operator namely the disabling operator. To illustrate such a disruption, we use a particularly M-net called M-net (TAbort) which contains a special kind of transition namely TAbort with an arbitrary (according to the whole of disrupted M-net places) number of entry-places and one exit-place. This transition is able to take into account this aborting by eliminating all token places of the disrupted behaviour net.
M( T Abort ›M` with ∀pε•t:
M`(p) = 0 and
M(p) ≥ 0
The semantics of disabling is expressed by the following scoping:
In Fig. 3, t1 and t2 are some hierarchical transitions which may be refined by the M-nets of B`1 and B2 behaviours respectively such that B1 = B`1; exit.
According to the refinement definition and disabling operator definition, y ≠ ∪ means that the exit-places of the refining M-net of T1 are not all marked (i.e., to the less one among them is empty).
Moreover, TAbort must have all the places of t1 refined in its entrance. Then, in the M-net which illustrate B`1 every entry or internal-place must have a dual status {x,e} or {x,i}, respectively.
Process instanciation: The standard form of a process instantiation is the synchronous instantiation. The following M-net is inserted for each process instantiation. The process is called by transition t1 after which the caller waits in place p1 until the process returns, at which point t2 is fired. The M-nets semantics is expressed by: M–net(P[G`1,...,G`l]) = Pcall.
CONCLUSION
Through the M-nets Algebra, a high level metalanguage and among simplest, we have presented a compositional semantics of a basic LOTOS specification. We have extensively made use of the modularity features of the M-net calculus and established thus a fully compositional model.
In this study it has only treated a simplified version of the language called basic LOTOS, while full LOTOS or simply LOTOS includes data structures that are derived from abstract data type language ACT ONE. The M-net formalism is insufficient for data type specification and another class of high level Petri-Boxes: A-nets allow such a specification. Thus, the future work in this aim should be a formal semantics for full LOTOS with A-nets.
The tool of verification and simulation for a composed M-nets is the PEP (Programming Environment based on Petri-nets) system, it`s an interactive system allowing a visualization of some complete, partial or step by step executions.