ABSTRACT
In this study, we propose a formal semantics for Basic LOTOS Language Of Temporal Ordering Specification). This is the subset of LOTOS where processes interact with each other by pure synchronizations, without exchanging values. In basic LOTOS we can appreciate the expressiveness of all the LOTOS process constructors (operators) 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 article we propose 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.
PDF Abstract XML References Citation
How to cite this article
DOI: 10.3923/itj.2007.110.116
URL: https://scialert.net/abstract/?doi=itj.2007.110.116
INTRODUCTION
LOTOS (Bolognesi and Brinksma, 1987) 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; Hugon, 1996), defined as the high level or coloured version of the Petri Box Calculus (PBC) (Best et al., 1992), is widely accepted to give semantics to concurrent systems and programming languages like B(PN)2 and SDL, cf. (Lilius and Pelz, 1996; Fleis Chhack and Grahlmann, 1997; Klaudel and Riemann, 1998; Hugon, 1996; Benzaken et al., 1998). 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) (Grahlmann, 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. 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) (Best et al., 1992). |
• | 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. 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:
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: 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 by 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 (otherwise). 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 anarityar (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: A :Ā≠ A, and ar (A) = ar(Ā)
We also assume 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(τ,...,τ ar (A) G [G1,...,Gar(A)] where A ε A and τj ε Var ∪ Val for 1≤ ι≤ ar (A); G ε G and Gi ε gatelist for 1≤ι≤ 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) (T xP) ∪ 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. |
Operations on M-nets: The composition operators on M-nets as defined by 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 ≠ (.,.) and yield a new transitions in N (Best et al., 1999). The operation will be defined a 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 (Klaudal, 1995).
The restriction operation N rs A removes from N all transitions that mention either A or ≠ and hence all synchronisation capabilities for A. 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 (Devillers et al., 19997, 1999; Klaudal and Riemann, 1998): N (Xi →Ni | iεl) allowing a hierarchical construction of M-net, means N where all Xi-labelled (hierarchical) | transitions are refined into (i.e., replaced by a copy of) Ni, for each i in the indexing set I. |
However, general refinement (Devillers et al., 1997) is not sufficient for our approach, in fact, knowing that a LOTOS system is described via a hierarchy of process definitions we must have a possibility to distinguish different instantiations of a process definitions and their behaviours. In order to satisfy this requirement, we use the general parametrised refinement concept (Devillers et al., 19997). The parameter mechanism is the mean by which a refining net interact with the area of the refined transition.
In this way, we add a formal parameter to hierarchical transition which deals with the concrete parameters of the call and return transitions labels.
• | The synchronization-lotos (Mekkl, 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: -P = P1 ∪ P2 -T = T1 ∪ T2 ∪ Tsy\(TG1 ∪ TG2 ) where Tsy is the set of transitions tsy arising through a basic synchronisation-lotos out of t1 and t2 over G such that:
t1 ε TG1, t2 ε TG2 and TG1 = T1 , TG2 = T2 ΓG, TG2 = T2ΓG λ = (λ1 ∪ λ2) Γ(P∧T) where α (tsy) = α (tl) = α (t2). |
• | 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 over all action names in the process definitions will insure the scoping. Thus, we get above global semantic formula: |
Withand
Where, γln (process) and γTn 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. It is easy that it consists of a call transition, a return transition and a body. The call transition is labelled 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 synchronisation with the Pc of the M-net for instantiation (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 M-net.
Thus in the M-net 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 t2.
In the sequel we suppose that the set Id (P)⊆ Val of instantiation identifiers is given.
Generaly a specification LOTOS is a hierarchy of processes. Therefore, we may have 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 Nl 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;
Nfj (id: ld (P) in charge for the initialization (call) and the termination (return) of each instanciation of Pj;
In the box Nfj (id: ld (P), the transition labelled χj is a hierarchical transition which is refined by the representative net of process definition body: NBPj (idj). The event of the transition t4 carried out by synchronization with the transition labelled by its complementary action belonging to the instanciation M-net (that we will 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 M-net.
Table 1: | Syntax of behaviour expressions in basic LOTOS |
This renaming is obtained using the function Pipgate-list. Finally, after refinement in, we obtain:
M-net (procdef) is obtained from the following expression:
M-net (procdef Pj (gatelist) = |
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) =
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.
Fig. 1: | semantic components of process definition Pj |
Fig. 2: | M-netstop, M-netexit and M-net of action over the gate G |
Fig. 3: | M-net (TAbort) and M-net (Abort) |
Fig. 4: | Process instantiation: Pcall |
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.
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 explicity 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 [] M-net (B2).
Parallel composition: LOTOS has three kinds of parallel operators (Table 1):
• | General case B1 | [{G1,..., G2}•{δ}]| B2where {G 1,..., 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 espressions 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 (||).
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:
M-net (B1 |[G1,..., Gm]| B2) = (M-net (Bl) |
## M-net (B2) sylotos {(G1•,..., •Gm)•δ} |
M-net (B1|**B2) = (M-net (B1)|*M-net (B2) sylotos {δ} |
M-net (B1|[G]|B2) = (M-net (B1)|* |
M-net (B2) sylotos {(G1•,..., • Gn)•δ} |
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) (Benzaken, 1998) over which no more interactions are possible.
M-net (hide Gl,..., Gr in B) = M-net (B) where Gl,..., Gr are renamed by i.
Disabling: B1 [> B2 in almost any OSI connection oriented protocol or service it is the case that the normal course of action can be disrupted at any point in time by events signalling 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 particulary 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 (p) = 0 and |
M (p)≥0 |
The semantics of disabling is expressed by the following scoping:
M-net (Bl [>B2) = M-net (Bl; exit) {>B2) |
= M-net (TAbort) [t1→M-net (Bl), |
t2 →M-net (B2)]|*M-net (Abort) sy |
Tabort rs Tabort [] M-net (Bl); M-netexit |
In Fig. 3 t1 and t2 are some hierarchical transitions which may be refined by the M-nets of B1 and B2 behaviours respectively such that; 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 B1 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 is fired. The M-nets semantics is expressed by:
M-net (P[G1,..., G1]) = Pcall |
CONCLUSIONS
Through the M-nets Algebra, a height 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 we have only treated a simplified version of the language called basic LOTOS, while full LOTOS or symply 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 height level Petri-Boxes: A-nets allows such a specification.
The tool of verification and simulation for a composed M-nets is the PEP (Programming Environment based on Petri-nets) system, its an interactive system allowing a visualization of some complete, partial or step by step executions.
REFERENCES
- Best, E., R. Devillers and J. Hall, 1992. The Box Calculus: A New Causal Algebra with Multi-Label Communication. In: Advances in Petri Nets, Rozenberg, G. (Ed.). Springer, Berlin/Heidelberg, ISBN: 978-3-540-55610-7, pp: 21-69.
CrossRefDirect Link - Best, E., W. Fraczak, R.P. Hopkins, H. Klaudel and E. Pelz, 1999. M-nets: An algebra of high-level Petri nets with an application to the semantics of concurrent programming langages. Acta Informatica, 35: 813-857.
CrossRefDirect Link - Devillers, R., H. Klaudel and R.C. Riemann, 1997. General refinement for high level petri nets. Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science, December 18-20, 1997, Springer-Verlag, London, UK., pp: 297-311.
Direct Link