Subscribe Now Subscribe Today
Research Article
 

A Semantics for the Control Part of Lotos



R. Mekki and B. Messabih
 
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail
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.

Services
Related Articles in ASCI
Similar Articles in this Journal
Search in Google Scholar
View Citation
Report Citation

 
  How to cite this article:

R. Mekki and B. Messabih, 2008. A Semantics for the Control Part of Lotos. Journal of Applied Sciences, 8: 2286-2292.

DOI: 10.3923/jas.2008.2286.2292

URL: https://scialert.net/abstract/?doi=jas.2008.2286.2292
 

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
Image for - A Semantics for the Control Part of 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: Image for - A Semantics for the Control Part of Lotos 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[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,T11) and N2 = (P2,T22) 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ΓG , TG2 = T2ΓG
- λ = (λ1 ∪ λ2P^T) where α(tsy) = α(t1) = α(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 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

Image for - A Semantics for the Control Part of Lotos

where, γ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.

Image for - A Semantics for the Control Part of Lotos
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 Image for - A Semantics for the Control Part of Lotoswhile the return transition is then correspondingly labeled with Image for - A Semantics for the Control Part of Lotos. 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 Pc of the M-net 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 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, 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;

Image for - A Semantics for the Control Part of Lotos in charge for the initialization (call) and the termination (return) of each instanciation of Pj;

In the box Image for - A Semantics for the Control Part of Lotos, the transition labeled χ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 labeled by its complementary action belonging to the instanciation M-net (see further) of the process according to the behaviour expression of the block; thus the list of the formal gates fgatelist in the net.

Image for - A Semantics for the Control Part of Lotos

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 Image for - A Semantics for the Control Part of Lotos, we obtains:

Image for - A Semantics for the Control Part of Lotos

M-net(procdef} is obtained from the following expression:

Image for - A Semantics for the Control Part of Lotos

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:

Image for - A Semantics for the Control Part of Lotos

where:

Image for - A Semantics for the Control Part of Lotos

with

Image for - A Semantics for the Control Part of Lotos

and

Image for - A Semantics for the Control Part of Lotos

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 ( || ).

Image for - A Semantics for the Control Part of Lotos
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:

Image for - A Semantics for the Control Part of Lotos

with [G1,...,Gn] = [gatelist]

Sequential composition:

Image for - A Semantics for the Control Part of Lotos

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.

Image for - A Semantics for the Control Part of Lotos
Fig. 3: M-net(TAbort) and M-net(Abort)

Image for - A Semantics for the Control Part of Lotos
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:

Image for - A Semantics for the Control Part of Lotos

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.

REFERENCES
1:  Benzaken, V., N. Hugon, H. Klaudel, E. Pelz and R. Riemann, 1998. M-net calculus based semantics for triggers. Proceedings of the 19th International Conference on Application and Theory of Petri Nets, LNCS 1420. June 22-26, 1998, Springer-Verlag London, UK., pp: 306-325.

2:  Best, E., H. Fleischhack, W. Fraczak, R.P. Hopkins, H. Klaudel and E. Pelz, 1995. A Class of Composable High Level Nets. In: Application and Theory of Petri Nets, LNCS 935, De Michelis, G. and M. Diaz (Eds.). Springer, Torino, pp: 103-120.

3:  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.
CrossRef  |  Direct Link  |  

4:  BuiThanh, C. and H. Klaudel, 2003. Encapsulation in an object-oriented notation based on modular Petri Nets. In: Simulation with Petri Nets, Workshop European Simulation and Modelling Conference, October 27-29 ESMC’2003. http://www.ibisc.Univ-evry. fr/pub/basilic/out/Publications/2003/Bk03/

5:  BuiThanh, C. and H. Klaudel, 2004. Object-Oriented Modeling with High Level Modular Peti Nets: Integrating Formal Methods. LNCS 2999, Springer, Berlin/Heidelberg, Germany, pp: 287-306.

6:  Devillers, R., H. Klaudel and R.C. Riemann, 2003. General parametrised refinement and recursion for the M-net calculus. Theor. Comput. Sci., 300: 259-300.
CrossRef  |  

7:  Fleischhack, H. and B. Grahlmann, 1997. A compositional Petri net semantics for SDL. Technical report. Universität Hildesheim.

8:  Garavel, H., 1990. Introduction to LOTOS. ftp://ftp.inrialpes.fr/pub/vasy/publications/cadp/Garavel-90-b.pdf.

9:  Grahlman, B., 1997. The PEP Tool. In: Computer Aided Verification Lecture Notes in Computer Science, Grumberg, O., (Ed.). Springer-Verlag, UK., pp: 440-443.

10:  Klaudel, H., 1995. Algebraic models, based on the Petri nets for the semantics of concurrent programming languages. Ph.D Thesis, University Paris-Sud, Orsay.

11:  Laudel, H.K. and R.C. Riemann, 1998. Application of general refinement to the semantics of a parallel programing language. Rapport de Recherche, L.R.I Universite de Paris-Sud.

12:  International Programme on Chemical Safety. 1985. Environmental health criteria 46. guidelines for the study of genetic effects in human population. WHO, Geneva, pp: 25-54.

13:  Mekki, R.H., 2000. A compositionnal semantics for basic LOTOS via a class of higth level Petri Nets. Magister Thesis, Computer Science Department, USTO.

©  2021 Science Alert. All Rights Reserved