International Journal of Electrical and Computer Engineering (IJECE) Vol.
No.
August 2017, pp.
ISSN: 2088-8708.
DOI: 10.
11591/ijece.
Formal Specification of QoS Negotiation in ODP System Abdessamad Jarrar.
Youssef Balouki.
Taoufiq Gadi Faculty of Sciences and Technologies Informatics.
Imaging and Modeling of Complex Systems Laboratory Settat.
Morocco
Article Info
ABSTRACT
Article history:
The future of Open Distributed Processing systems (ODP) will see an increasing of components number, these components are sharing resources.
In general, these resources are offering some kind of services.
Due to the huge number of components, it is very difficult to offer the optimum Quality of service (QoS).
This encourages us to develop a model for QoS negotiation process to optimize the QoS in an ODP system.
In such system, there is a High risk of software or hardware failure.
To ensure good performance of a system based on our model, we develop it using a formal method.
In our case, we will use Event-B to get in the end of our development a system correct by construction.
Received Feb 9, 2017 Revised Apr 19, 2017 Accepted May 3, 2017 Keyword:
Event-B Formal method Negotiation ODP Quality of service Refinement processus Copyright A 2017 Institute of Advanced Engineering and Science.
All rights reserved.
Corresponding Author:
Abdessamad Jarrar.
Faculty of Sciences and Technologies.
Computing.
Imaging and Modeling of Complex Systems Laboratory.
FST Settat.
Km 3.
: 577 Route de Casablanca.
Morocco.
Email: Abdessamad.
jarrar@gmail.
INTRODUCTION
The evolution of telecommunications technology and the structure of organizations have led to the emergence of complex distributed systems.
These systems are distributed structures whose components, both hardware and software, are of different types.
In some systems, these components are developed by different actors acting independently of each other.
The assembly of such components gives rise to highly heterogeneous systems.
The applications that support these systems are themselves composed of distributed The interaction between these application components is one of the aspects of the distributed Specifically, the distributed processing correspond to different aspects of information processing in which specific components can be located in different places, during this process the communication between components may be delays or failures.
This means that this kind of systems needs to be developed carefully due to its complexity .
This motivates us to model it using a formal method to ensure the correctness of our system and obtain a very strong assurance of bugAos absence.
Formal methods are a particular kind of mathematically based techniques for the specification .
, .
, development and verification of software and hardware systems .
There are a variety of formal methods such as language Z, a specification in Z is a predicate, the specification of invariants and the specification of operations have the form of a predicate.
There is also B-method which is a method of software development based on B, a toolsupported formal method based on an abstract machine notation, used in the development of computer It was originally developed by Jean-Raymond Abrial .
In this paper, we will use Event-B .
since it allows us to prove that our system is correct by construction basing on proofs obligations.
These proofs are done automatically by a tool called Rodin .
Event-B is also based on refinement which means creating an abstract model and enriching it in a multiple steps by adding more details to get a more concrete model .
In every refinement, we prove that the system is correct and it does not contradict with the previous one, whereby the resulting system is correct by Journal homepage: http://iaesjournal.
com/online/index.
php/IJECE A ISSN: 2088-8708 construction .
In the beginning, we present the proposed negotiation approach, this approach is based on Then, we define the system requirement along two axes: FUN and ENV.
After that, we present our refinement strategy that we will use after that to specify our system.
Lastly, we end this paper with a conclusion presenting an abstract about the work done and our expectation about future works.
RELATED WORKS
AiUsing Event B to Specify QoS in ODP Enterprise LanguageAn .
like our work, is specifying QoS negotiation using event-B, it presents a specification for the different actors of the system and their states and it also present negotiation values.
However, it doesnAot present a specification of how the system acts exactly such as how the system is able to negotiate with multiple servers.
AiEnd-to-end QoS negotiation in network federationsAn .
is another work presenting QoS negotiation, it presents a good specification of the negotiation process, and in addition it presents a mathematical modeling.
Yet, mathematical model doesnAot prove that the specification is correct.
Also, it limits the study in telecommunication domain.
AiAn example of dynamic QoS negotiationAn .
presents an example of QoS negotiation applied to a video streaming application, this example is presented with mathematical models and statistics results.
The same as the previous paper, there is nothing proving the correctness of the system.
Our work is presenting a formal specification using Event-B, this allows us to ensure the correctness of our system using poof obligations, it also presents a modeling of negotiation in more details.
Also, our work is proved using Rodin platform .
which avoid human mistakes during proving proof obligations.
NEGOTIATION APPROACH
Quality of Service (QoS) is a management concept that aims to optimize network resources or process and ensure good performance of an Open Distributed Processing (ODP) system, this concept is fundamental in many fields such as transmission protocols .
, routing algorithms .
, resources allocation algorithms .
and web service .
In our negotiation process, we will base our study on the trader concept .
This means that in addition of the client and servers, we will have a third actor, it is the trader.
The trader is playing the role of a controller who is able to get the best QoS possible for a client.
In the beginning, a client propose a value of quality of service P to the trader, the trader may modify the QoS proposed by the client or not, after that the trader send the value PAo of QoS to the server, when the server gets the required value it may either refuse the request or may propose the value V that it may offers, at this stage the trader will either modify the value proposed by the server or returns it directly to the client, if the client is satisfied with the proposed value he accepts it or else he refuses it, in this case the trader will automatically start negotiation with another server and proceed in the same way.
The Figure 1 below presents the process of negotiation with a server basing on a UIT form .
Figure 1.
Negotiation Process .
FORMAL SPECIFICATION OF QOS NEGOCIATION Requirement Document To present the requirement document correctly, we present it along two main axes.
The first axis expresses the main functions of system "FUN", and the second describes these functions and provides some details regarding the environment "ENV".
We present our requirement document as follows:
The system allows for the negotiation of QoS between a client and one or more servers IJECE Vol.
No.
August 2017 : 2045 Ae 2053
FUN 1
IJECE
ISSN: 2088-8708
ENV 1: The trader is an intermediate between client and server.
Negotiation end if the client accepts the QoS or if he refuses it FUN 2 ENV 2: A client can be in one of three states .
ropose, accept or refus.
The client can only accept negotiation if the trader proposes a value of quality of service FUN 3 ENV 3: A trader can either propose a value of QoS or refuses to offer the service.
the trader can only refuse negotiation if all the servers refuse to offer any QoS or if the client
refuse all the proposed values of QoS
FUN 4
ENV 4: a server can propose or refuse to offer any QoS
The value proposed by the server is always less than or equal the value given by the trader
FUN 5
ENV 5: values of QoS are always positive.
The trader always propose values less than or equal the value proposed by the client
The client propose the value he wants, then the trader seeks the best value less than or equal to that value in all servers FUN 6
FUN7
Refinement Strategy After specifying our negotiation process correctly, we present our refinement strategy.
We start by creating an abstract model .
irst refinemen.
containing the principal functions of our system, then we will enrich it by adding more function and environment assumptions .
econd refinement and third refinemen.
more details, here is our refinement strategy:
First refinement: In the beginning, we present the various actors states .
lient, trader and server.
and the basic logic of the system (FUN 1.
FUN 2.
FUN 3.
FUN 4.
ENV 1.
ENV 2.
ENV 3 and ENV .
Second refinement: in this refinement, we include negotiation values and how the actors may change it while negotiating with a server (FUN 5.
ENV 5 and ENV .
Third refinement: lastly, the system is able to negotiate with multiple servers (FUN .
First Refinement: Specifying Actors States As it is mentioned before, we start by modeling the various states of the system actors.
Here is our first context of the first refinement:
CONTEXT
SETS
STATE
CONSTANTS
AXIOMS
axm1:partition(STATE,.
, .
) END In this context which is the static part of a refinement, we define the set STATE as a partition of the all the possible states in the system of an actors.
In addition, we add an additional state that we have called AiwaitAn.
this state is the initialization state.
We present the dynamic part of the first refinement .
start by the invariant that are the properties that must be preserved during system occurrence:
Formal Specification of QoS Negotiation in ODP System (Abdessamad Jarra.
A ISSN: 2088-8708
VARIABLES
S_st C_st T_st INVARIANTS S_st OO STATE S_st O accept C_st OOSTATE T_st OO STATE T_st O accept C_st = accept Ne T_st = propose T_st = refuse Ne C_st O accept T_st = refuse Ne S_st = refuse S_st = propose Ne T_st = propose In these invariants, we define S_st (Server stat.
as an element of STATE that is not equal accept, the same go for T_st (Trader stat.
as the server and the trader are not allowed to accept the negotiation, the client is the only actor that may accept the negotiation this is why C_st may be equal any state.
In addition, we present some invariant that control the possible state combinations, for example, if the client is in the accept state the trader must be in the state propose .
, which mean that a client cannot accepts a negotiation if the trader did not proposes a QoS value.
Now we can initialize our variable with AiwaitAn value.
INITIALISATION:
THEN
S_st Oi wait
C_st Oi wait
T_st Oi wait
END
Beside the initialization event we have more events that are able to change the states of the actors while preserving all the invariants.
Client_propose is the event that starts a new negotiation.
we can start a new negotiation only if we end the previous one, which means that the trader is not in the state AiproposeAn.
Client_propose:
WHERE
C_st = wait T_st O propose C_st Oi propose THEN END When a client proposes a value of QoS, the trader switches his state to AiproposeAn to start negotiation with servers.
Trader_propose:
WHERE
C_st = propose T_st Oipropose THEN END The server proposes or refuses negotiation if and only if the trader proposes.
Server_refuse:
WHERE
T_st = propose S_st Oi refuse THEN END The only case where the trader will refuse negotiation is when all servers refuse negotiation, and then the trader ends negotiation and informs client.
Trader_refuse:
WHERE
C_st = propose S_st = refuse T_st Oi refuse C_st Oi refuse THEN END The client refuses a negotiation if he is not satisfied with negotiation value proposed by the trader.
IJECE Vol.
No.
August 2017 : 2045 Ae 2053
IJECE
ISSN: 2088-8708
Client_refuse:
WHERE
C_st = propose T_st = propose C_stOi refuse T_st Oi refuse S_stOi refuse THEN END Also, if the client is satisfied with the proposed value by the trader, he accepts negotiation.
Client_accept:
WHERE
T_st = propose THEN C_st Oi accept
END
Second Refinement: Modeling Negotiation Values In this refinement, we present the negotiation values.
A client propose a value of quality of service P to the trader, the trader may modify the QoS proposed by the client or may keep it, after that the trader send the value PAo of QoS to the server, when the server get the required value it may either refuse the request or may propose the value V that it is able to offer, at this stage the trader will either modify the value proposed by the server or return it directly to the client.
Before modeling these events, we present the context below presenting the maximum value of QoS that a server may offer Vserver_max:
CONTEXT
EXTENDS
CONSTANTS
Vserver_max AXIOMS
Vserver_max OOEi
Vserver_max > 0
END
In machine1, we have new variables representing the negotiation values (Vclient.
Vtrader.
Vserver and Vservice which is the value of QoS offered in case of accepting the negotiatio.
Moreover, we have additional invariant for the negotiations values:
INVARIANTS
Vclient OOEi Vserver OOEi Vtrader OOEi Vservice OOEi Vclient Ou Vtrader Vtrader Ou Vserver T_st = propose Ni Vtrader O 0 S_st = propose Ni Vserver O 0 (C_st = propose O C_st = accep.
Ni Vclient O 0 Vserver O Vserver_max Furthermore, we refine the events of refinement 0 by adding actions responsible for dealing with QoS values such as these actions setting negotiation values to 0 in the initialization event:
Vclient Oi 0 Vserver Oi0 Vtrader Oi0 VserviceOi 0 The value proposed by the client Vclient must be a not null natural number.
Formal Specification of QoS Negotiation in ODP System (Abdessamad Jarra.
A ISSN: 2088-8708 Client_propose:
ANY
val OOEi
val O 0
C_st Oi propose Vclient Oi val
WHERE
THEN
END
The value proposed by the trader must be a positive number less than or equal the value proposed by the client.
Trader_propose:
ANY
WHERE
C_st = propose val OOEi
val O Vclient
val Ou Vserver
val O 0
T_st Oipropose Vtrader Oi val
THEN
END
A server proposes a value less than or equal the value proposed by the trader, and this value is always less than or equal a predefined maximum value of the Qos.
Server_propose:
ANY
WHERE
T_st = propose val OOEi
val O Vtrader
val O 0
val O Vserver_max S_st Oipropose Vserver Oi val
THEN
END
When a trader proposes a value of QoS, the server may be unable to offer any QoS, in this case the server refuses the process of negotiation.
Server_refuse:
WHERE
T_st = propose S_st Oi refuse Vserver Oi 0
THEN
END
If a server refuse to offer a QoS, the trader try to negotiate with another server until it find a valid QoS, however in some cases all the servers are unable to offerQoS, which mean that the trader will stop negotiation, which mean that we reset the value of Vtrader and Vclient to 0 in the event Trader_refuse:
Vtrader Oi 0 VclientOi 0 Even if the trader find a server that may offer a Qos, the client may be not satisfied, in this case the client may refuse the negotiation by resetting all the negotiation values to 0 in the event Client_refuse:
Vclient Oi 0 Vtrader Oi 0 Vserver Oi 0 In the other hand, if the client is satisfied with the offered QoS, he may accept negotiation.
In this case, the value of service will be the value that the trader proposes, which means that we have one additional action in the event Client_accept:
IJECE Vol.
No.
August 2017 : 2045 Ae 2053
IJECE
ISSN: 2088-8708
Vservice Oi Vtrader Third Refinement: Negotiation with Multiple Servers In this last refinement, we allow the system to negotiate with multiple servers.
In other words, when the client gets the QoS value proposed he may be not satisfied with it and refuses the negotiation.
In this case, the trader starts negotiating with another server that may offer a better QoS.
To model this, we need to define a set of servers in our system illustrated in the context below:
CONTEXT
EXTENDS
SETS
Servers AXIOMS
Servers O OI
END
Similarly, we define new two variables.
The first variable is server which represents the current server that we are negotiating with.
The second is Servers_Not_Tested which represents the set of servers that we have not negotiated with yet.
More than that, we have additional invariant:
server OO Servers Servers_Not_Tested OOEo(Server.
In the same way as the previous refinement, we refine also the events of machine 1.
In the beginning, we refine the initialization event:
INITIALISATION:
THEN
server :OO Servers Servers_Not_Tested Oi Servers END In the beginning of every new negotiation, the client proposes a QoS as mentioned before, at this stage, we initiate the set Servers_Not_Tested as all the servers of our network in the event Client_propose :
Servers_Not_Tested Oi Servers The trader is the one responsible for choosing the server to negotiate with.
this server is chose from the set Servers_Not_Tested, which mean that we need to check if this set is not empty in the event Trader_propose using the following guard:
Servers_Not_Tested O OI Also, this action picks a server from Servers_Not_Tested:
server :OO Servers_Not_Tested When a server refuses to offer a QoS, we remove it from Servers_Not_Tested to ensure that we wonAot negotiate with the same sever over and over again.
The action allowing removing the server from Servers_Not_Tested in the event Server_refuse is the following:
Servers_Not_Tested Oi Servers_Not_Tested On.
The trader refuses negotiation if and only if all the servers refuse to offer a QoS which mean that we removed all the servers from Servers_Not_Tested, this mean that Servers_Not_Tested is empty.
This means that the Trader_refuse will never be occurred unless Servers_Not_Tested is empty.
this is done by the following guard:
Servers_Not_Tested=OI The client accepts the negotiation if there is a server in Servers_Not_Tested that may offer a QoS and the client is satisfied with it.
This means that we will have a new guard in the event Client_accept:
server OO Servers_Not_Tested PROVING SYSTEM CORRECTNESS Proof obligations are a set of evidence that ensures the validity of the system, the most important among them is the preservation of invariants proofs that validates the preservation of all the invariant condition before and after each event, all this can be done manually.
Most of the proofs are easy and are not Formal Specification of QoS Negotiation in ODP System (Abdessamad Jarra.
A ISSN: 2088-8708 the kind of demonstrations that could interest a mathematician because the difficulty of modeling in event-B is not the complexity of proof but demonstrations of consistency despite the huge number of events and invariants, all events must preserve all the invariant.
This mean that the problem is that the amount of proof to prove is very big, in our case we have 21 invariants .
in machine 0, 10 in the machine 1 and 2 for the machine .
and we have 10 events this mean that we have 210 proof to be done.
Luckily there is a platform to do the most of these proofs automatically, this framework is called Rodin.
The Rodin platform is an IDE based on Eclipse for Event- B which provides effective support for refinement and mathematical proof.
The platform is open source, contributes to the Eclipse platform and is more extensible with plugging very effective (Atelier.
ProB .
In the Table 1 below the statistics of proofs done by Rodin:
Table 1.
Proof Statistics Elements Qosnegot Context0 Context1 Context2 Machine0 Machine1 Machine2 Total Auto Reviewed Undischarged CONCLUSION we have developed the process of negotiation of QoS between objects in an ODP system, using the trading function.
We have proposed to introduce a dynamic trading assistant in the user's terminal to help, firstly, to choose the best service provider and, secondly, to dynamically negotiate the quality parameters of service (QoS) responsive to the user's requirements and application.
The model we have developed is based on the formal method Event-B.
The interest of the Event-B in our study lies in its modeling to formally express properties validated by evidence during the design of system models, but also in its refinement principle to master the complexity of the system by progressive and safe development.
For future works, we are working on specifying formally aircraft landing process.
we also will develop a model of an abstract complex adaptive system.
REFERENCES