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 subprocesses. 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 Mnets 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 Mnets is their full compositionality thanks
to their interfaces and a set of various net operations defined semantics
for them. In fact, Mnets 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). Mnets
just offer these features. We have chosen to translate basic LOTOS specifications
into the algebra of modular highlevel Petri nets: the Mnets (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 Mnets for each syntactic operator of basic LOTOS. Using our approach
a property of a basic LOTOS specification is checked as follows:
• 
The Mnet semantics of the basic LOTOS specification
is calculated 
• 
The Mnet is unfolded into a Petri box (a special lowlevel 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 blockstructured programming language. The structure
of basic LOTOS specification is:
specification 
specname [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, B_{1}, B_{2} stand any behaviour
expression; G, G_{1}, G2,…,G_{n} are elements of
a finite alphabet gate list.
Remark: As we will see farther, the parallel operator `` take
an important part in the Mnets algebra; thus, in order to avoid confusion
we reserve this notation for the composition of Mnets. 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.
Mnets: The Mnets 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 Mnets and coloured nets is that
Mnets 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), Mnets 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 Mnet carries an inscription of the form inscription = (label
 annotation). 
Thus, every place and transition of an Mnet 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: and ar(A) = ar(Ā)
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[G_{1},…,G_{ar(A)}] where A ε A and τ_{j} ε Var ∪ val for 1 ≤I≤ar(A);
G ε G and G_{i} ε gatelist for 1≤i≤ar(G).
Definition of Mnets: An Mnet 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 Mnets: The composition operators on Mnets 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 Mnet 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 Mnet 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 Mnet 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.
Mnet model extensions: In order to adapt the Mnet model for
a basic LOTOS compositional semantics, the operations on Mnets must be
extended to some other operators such that:
• 
The Mnet refinement (Reimann et al., 2003; Devillers
et al., 2003; Klaudel and Riemann, 1998): N[X_{i} ←
N_{i}i ε I] allowing a hierarchical construction
of Mnet, means N where all X_{i}labeled (hierarchical) 
transitions are refined into (i.e., replaced by a copy of) N_{i},
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 synchronizationlotos (Mekki, 2000) sy_{lotos} is defined such that:
Let two Mnets N_{1} = (P_{1},T_{1},λ_{1})
and N_{2 }= (P_{2},T_{2},λ_{2})
and let G an action gate symbol.
(N_{1}N_{2})sy_{lotos} = (P,Tλ)
where:
 P = P_{1} ∪ P_{2
} T = T_{1} ∪T_{2} ∪ T_{sy}\(T_{G1} ∪ T_{G2 }) where T_{sy} is the set of transitions
t_{sy} arising through a basic synchronisationlotos out
of t_{1} and t_{2} over G such that:
t_{1} ε T_{G1} , t_{2} ε
T_{G2} and T_{G1} = T_{1}Γ_{G} , T_{G2} = T_{2}Γ_{G
} λ = (λ_{1} ∪ λ_{2})Γ_{P^T)} where α(t_{sy}) = α(t_{1}) = α(t_{2}) 
• 
The relabelling function (Mekki, 2000): ∏^{p}_{gatelist} which is applied to an Mnet N, is parametrised with a name of process
definition (P) and a list of gate names (gatelist). It does the following
substitution for each gate name G_{i} ε gatelist
in N. 
Semantics of a basic LOTOS specification: A semantics of basic
LOTOS specification will be defined associating one Mnet to each process
definition (avowed in the where clause) its behaviour expression.
The initialization and clearing of each process definition The Mnet
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 Mnets 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)
With
where, γ_{n}^{I} (processes) and γ_{n}^{T}
(processes) are the auxiliary Mnets for initialization and termination
of scoping.
In the sequel, the other Mnets 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 P_{j} 
It is easy that it consists of a call transition,
a return transition and a body. The call transition is labeled with while
the return transition is then correspondingly labeled with .
The control flow in the body is represented by the black to which moves
through the body representing the different actions that the process executes.
The call of the process is equivalent to the synchronization with the
P_{c} of the Mnet for instantiation (which will be defined later,
cf. Fig. 4). However if several instantiations of the
process are active at the same time, this simple scheme does not work.
The reason for this is, that since the control tokens have no identity,
we may not distinguish between them and so the causal relations between
the control and the process instantiations may be broken. We propose to
solve the problem by using colored tokens (id) as indexes to distinguish
between the instantiations, allowing to fold the different instantiations
of the process into one Mnet. Thus in the Mnet construction of process
definition semantics (Fig. 1), we allow Id (p) (the
instantiation set) as type for internal places and id as concrete parameter
for actions of hierarchic transition t_{2}.
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 P_{j} a process definition identifier at the
jth level of overlap (with 1≤#m where m is the maximal depth of overlap).
The box Mnet (procdef) of a process definition declared at the level
of overlap depth j is obtained by successive refinements in the operator
Mnet.
N_{I} NI_{j} (id_{1}:Id(P),...,idj_{–1}:Id(P))
of semantic components of P_{j} where:
Ni_{j} (id_{1}:Id(P),...,id_{j–1}:Id(P))
in charge for the management of instanciations P_{j};
in charge for the initialization (call) and the termination (return) of
each instanciation of P_{j};
In the box ,
the transition labeled χ_{j} is a hierarchical transition
which is refined by the representative net of process definition body:
NBP_{j}(id_{j}). The event of the transition t_{4}
carried out by synchronization with the transition labeled by its complementary
action belonging to the instanciation Mnet (see further) of the process
according to the behaviour expression of the block; thus the list of the
formal gates fgatelist in the net.
must be renamed in list of effective gates belonging instanciation Pcall
Mnet.
This renaming is obtained using the function Pi^{p}_{gate–list}.
Finally, after refinement in ,
we obtains:
Mnet(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:
Mnet(process definitions) = ∏^{k}_{n=1}P_{n}
and the action symbols for scoping are:
where:
with
and
Behaviour expression Mnet: 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 Mnets 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:
Mnet (G ; B) = Mnet(G); Mnet(B) where Mnet(G) is given in Fig.
2.
Choice: Mnet(B_{1}[]B_{2} = Mnet (B_{1})
Mnet(B_{2})
Parallel composition: LOTOS has three kinds of parallel operators
(Table 1):
• 
General case B_{1}[{G_{1},...G_{2}}∪{δ}]B_{2}
where {G_{1},...,G_{m}} a set of userdefined gates
called synchronization gates of B_{1} and B_{2} 
• 
Pure interleaving B_{1}[G]B_{2} when the set of
synchronization gates is only δ. 
• 
Full synchronization B_{1}[G]B_{2} when the set
of synchronization gates is the set of all gates appearing in both
behaviour expressions including δ. The Mnets semantics of parallel
operators is carried out in two stages: Concurrency is expressed applying the parallel operator
of Mnets algebra (  ). 

Fig. 2: 
Mnet_{stop }, Mnet_{exit} and Mnet
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 t_{1} and t_{2} belonging respectively
to Mnets B_{1} and B_{2} must synchronize through sy_{lotos}
if they have in their respective labels the same action gate symbol belonging
to the set of synchronization gates of specified operator, either [G_{1},...,G_{2}]
for the first case and [G] for the second. Thus, the semantics of this
three operators is:
with [G_{1},...,G_{n}] = [gatelist]
Sequential composition:
Hiding: The operator hide … in allows one to transform some
observable actions of a process into unobservable ones. The Mnets 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 G_{1},...,G_{r} in B) = M–net(B)
where G_{1},...,G_{r} are renamed by i.
Disabling: B_{1}[>B_{2}. In almost any OSI
connection oriented protocol or service.

Fig. 3: 
Mnet(TAbort) and Mnet(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 Mnet called Mnet (TAbort) which contains a special
kind of transition namely TAbort with an arbitrary (according to the whole
of disrupted Mnet places) number of entryplaces and one exitplace.
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, t_{1} and t_{2} are some
hierarchical transitions which may be refined by the Mnets of B`_{1}
and B_{2} behaviours respectively such that B_{1} = B`_{1};
exit.
According to the refinement definition and disabling operator definition,
y ≠ ∪ means that the exitplaces of the refining Mnet of T_{1}
are not all marked (i.e., to the less one among them is empty).
Moreover, TAbort must have all the places of t_{1} refined in
its entrance. Then, in the Mnet which illustrate B`_{1} every entry or internalplace 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 Mnet is inserted for
each process instantiation. The process is called by transition t_{1}
after which the caller waits in place p_{1} until the process
returns, at which point t_{2} is fired. The Mnets semantics is
expressed by: M–net(P[G`_{1},...,G`_{l}]) = Pcall.
CONCLUSION
Through the Mnets 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 Mnet 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 Mnet formalism
is insufficient for data type specification and another class of high
level PetriBoxes: Anets allow such a specification. Thus, the future
work in this aim should be a formal semantics for full LOTOS with Anets.
The tool of verification and simulation for a composed Mnets is the
PEP (Programming Environment based on Petrinets) system, it`s an interactive
system allowing a visualization of some complete, partial or step by step
executions.