Formalizing and checking web service discovery models using B

 B 79
of reliability for a Web Service. Reliability also refers to the assured and ordered delivery for
messages being sent and received by service requesters and service providers.
Availability. Availability is the quality aspect of whether the Web service is present or
ready for immediate use. Availability represents the probability that a service is available.
Larger values represent that the service is always ready to use while smaller values indicate
unpredictability of whether the service will be available at a particular time.
S ecurity. Security is the quality of providing confidentiality and non-repudiation by au-
thenticating the parties involved, encrypting messages, and providing access control. Security
has added importance because Web service invocation occurs over the Internet. The service
provider can have different approaches and levels of providing security depending on the service
requester.
3. FORMALIZING AND CHECKING WEB SERVICE DISCOVERY
MODELS
From the similarity in web service discovery models and the B refinement mechanism.
We propose in this section an approach to formalize web service discovery models using B
notation. Particularly, this formalization allows us to prove automatically the model by using
B provers.
3.1. Formalizing web service discovery models
The web service discovery process requires a language such that OWL-S [4], which can
be used to encode Web service capabilities for advertisement and for requests. Furthermore,
discovery requires a matching process that compares the advertisements with the requests to
verify whether they describe matching capabilities. An advertisement matches a request when
all the inputs, outputs of the request are matched by the inputs, outputs of the advertisement,
respectively. Additionally, precondition, postcondition and other QoS of service advertisement
need to match the ones of service requester. Note that, OWL-S supports both views, requester
and provider, of the capabilities of Web services. Additionally, OWL-S is based on formal
semantics, it can fully represents the inputs, outputs and QoS of the service. As a result, we
use OWL-S to express web service semantics in our work.
Hình 3.2. Formalizing requester requirements by a B abstract machine
Figure 3.2 illustrates the transformation of web service requester requirements to a B
abstract machine. The name of service, input and output desired are transformed to the name
80 TRUONG NINH THUAN, TRINH THANH BINH, VAN HIEU VU
of operation, input parameters and output parameters, respectively. The precondition and
effects of web service are formalized by precondition and body of the operation in the B
abstract machine. The others QoS of web service desired are formalized in an operation called
serviceQuality.
An OWL-S Profile (has also been called service capability advertisement) describes a
service as a function of three basic types of information: what organization provides the service,
what function the service computes, and a host of features that specify characteristics of the
service. The three pieces of information are reviewed in order below.
Firstly, the provider information consists of contact information that refers to the entity
that provides the service. For instance, contact information may refer to the maintenance
operator that is responsible for running the service, or to a customer representative that may
provide additional information about the service.
Secondly, the functional description of the service is expressed in terms of the transforma-
tion produced by the service. Specifically, it specifies the inputs required by the service, the
outputs generated, precondition required by the service and the expected effects that result
from the execution of the service.
Finally, the profile allows the description of a host of properties that are used to describe
features of the service. The first type of information specifies the category of a given service.
The second type of information is quality rating of the service: some services may be very
good, reliable, and quick to respond; others may be unreliable, sluggish, or even malevolent.
Before using a service, a requester may want to check what kind of service it is dealing with;
therefore, a service may want to publish its rating within a specified rating system.
From the description of OWL-S Profile, we propose to formalize them using a B refinement
machine as shown in Figure 3.3. An input specifies the information that the service requires
to proceed with the computation. For example, a book-selling service could require the credit
card number and bibliographical information of the book to sell. The input is described in
OWL-S as follows.
An output is a type of parameter and is a property of a profile. An output specifies what
is the result of the operation of the service, it is expressed:
The inputs and outputs in OWL-S Profile are reprensented by input and output parameters
of the operation in the B refinement machine, respectively (Figure 3.3).
Precondition represents a condition that is expected for the service to work appropriately.
For example, a precondition is that some money is available to pay for some goods, or that
the goods are available and so on. The precondition is described in the form as follows.
FORMALIZING AND CHECKING WEB SERVICE DISCOVERY MODELS USING B 81
Hình 3.3. Formalizing provider capabilities by a B refinement machine
Effect represents conditions that are expected to result after the execution of the service. For
example, a credit card is charged, goods are delivered as so on. The description of effect is as
the following.
hasEffect
The precondition and effects of the web service are formalized by precondition and body of the
operation in the refinement machine (Figure 3.3). The quality rating of a service will be a very
important issue in the selection of services. The quality rating has two fields: ratingName and
rating: ratingName that specifies the name of the rating service; rating is the rating assigned
to the service. An example of rating service is presented as below.
SomeRating
QoS of web service provider, including the estimation ofmaxResponseTime and averageResponseTime,
are formalized in an operation called serviceQuality presented in the refinement machine (Fig-
ure 3.3).
3.2. Checking capability matching in WSD model through the B refinement
mechanism
In a WSD model, capability matching compares the capabilities provided by any of the
advertised services with the capabilities needed by the requester. The goal is to find the
advertiser that produces the results required for the requester.
In order to simplify the development of the system, the method in B machines uses the same
notation for all the stages of the development, that goes on for successive refinement steps. B
refinement provides a way to construct stronger invariants and also to add details in a model.
It is also used to transform an abstract model in a more concrete version by modifying the
82 TRUONG NINH THUAN, TRINH THANH BINH, VAN HIEU VU
state description. Increasingly, proof obligations defined in B refinement relation allow us to
check that preconditions and postconditions of lower level operations conform to preconditions
and postconditions of higher level operations. Recall that, the abstract state variables, xx , and
the concrete ones, xx ′, are linked together by means of a gluing invariant InvM ′ defined in the
refinement machine.
Formalizing WSD model using B refinement, as a result, enables us to check the identity of
the name, input and ouput of web service requester required and service provider. Additionally,
as presented in the paper [15], the degree of matching can be differentiated by four levels:
exact, plug in, subsumes, fail. Depending on the degree of matching, we can also check the
correlativeness of preconditions, effects and QoS between requirements of web service requester
and capabilities of the one provider.
4. CASE STUDY
We illustrate our approach by considering a simple system of Tax calculation web service.
This one build a web service that can calculate sales tax amounts for goods. With the devel-
opment of applications processing data based Internet resources, such sales tax services are
going to be critical for calculating tax amount of imported goods.
This web service is described as follows. The calling application must provide a valid type
as well as quantity of goods. The returned result is the amount of money calculated basing
on tax regulations. Below table shows a capability description for the Tax Calculation web
service provider.
Context: Tax Calculation;
Types: Goods = {Tobacco,Wine,Laptop},
Money = Real;
Input: typeOfGoods:Goods;
quantity:Integer;
Output: TaxAmount:Money;
Precondition: quantity > 0;
Effect: TaxAmount =
taxOf(typeOfGoods)*quantity;
TextDescription: calculating tax amount for imported goods.
On the other hand, the rating system declares that the max response time of the web service
provider is 8 ms, the availability is at least 99% and reliability is at least 98% in the 100-degree
rating scale system.
Supposing that, in the side of the requester, one requires a web service with the context,
types, inputs, outputs, precondition are similar as information described above. The requester
does not know the effect of the web service provider, they only require the result of web service
is a value of Money type. The also require that, reliability of the web sevice is at least 98%,
availability is at least 98% and the max response time is below 10 ms.
4.1. Describing in OWL-S
As introduced in Subsection 3.1, Semantic web services are described using OWL-S (for-
merly DAML-S) which is an OWL ontology with three interrelated subontologies, known as
the profile, process model, and grounding. In brief, the profile is used to express "what a ser-
vice does", for purposes of advertising, constructing service requests, and matchmaking; the
FORMALIZING AND CHECKING WEB SERVICE DISCOVERY MODELS USING B 83
process model describes "how it works", to enable invocation, enactment, composition, moni-
toring and recovery; and the grounding maps the constructs of the process model onto detailed
specifications of message formats, protocols, and so forth (normally expressed in WSDL).
Because of the similarity of description in OWL-S between web service provider and web
service requester, we consider only the description of the Tax Calculation web service provider.
We representes inputs, outputs, precondition and effect of the web service in OWL-S Profile
and these are then refered to OWL-S Process as the following:
(and (member ?TypeOfGoods ?Goods)
(and (member ?Quantity ?Integer)
(> (?Quantity 0))))
(= ?TaxAmount
(* (value ?taxOf ?TypeOfGoods)
?Quantity))
...
Note that, in this description, the precondition and effect of web service are expressed by
Knowledge Interchange Format (KIF) [5]. Goods is a set containing all product names in the
tax table, taxOf is a function, from the Goods type to the Money type, applied to calculate
the tax of goods ruled by government. It is described in OWL-S as follows.
...
84 TRUONG NINH THUAN, TRINH THANH BINH, VAN HIEU VU
4.2. Formalizing and checking in B notation
Applying the transformation rules presented in Section 3, we formalize the description of
the Tax Calculation web service provider and requester presented in Figure 4.5. The requester
is described byWS Requester abstract machine and the provider is introduced in WS Provider
refinement machine which refines WS Requester machine. These machines see (SEES clause)
the Types machine which declares sets used in the model (Figure 4.4).
MACHINE Types
SETS GOODS = {Tobacco,Alcohol , ...}
CONCRETE CONSTANTS
MONEY ,
AVAILABILITY ,
RELIABILITY , ...
PROPERTIES
MONEY ⊆ INT ∧
AVAILABILITY ⊆ NAT ∧ AVAILABILITY =
1..100 ∧
RELIABILITY ⊆ NAT ∧ RELIABILITY = 1..100 ∧
...
END
Hình 4.4. Types machine
In this model, the rating system uses 100 levels (as supposed above). Each QoS element of
the web service thus gets the value from 1 (lowest) to 100 (highest) (see Figure 4.4). The effect
in the method used to calculate the tax amount of requester (calcul Tax ) requires merely the
return value is belong to theMoney type 1. The one in service provider is a formula calculating
the tax amount.
The B provers will check if the return value of the formulation in the refinement machine
is belong to Money type, corresponding with the output value of the method calcul Tax in
the abstract machine. This is done based on proof obligations of B refinement. By this way,
we can check the correlation of the value of QoS between web service requester and provider,
defined in gluing invariant of the refinement machine.
We proved our B model with B4free tool [7], 10 proof obligations are generated for the
WS Provider refinement machine, 80% (8) of them are proved automatically and the rest are
proved interactively. Other proof obligations in the model are proved automatically.
5. RELATED WORK
The impact of formal methods in SOA has been confirmed [6]. Actually, however, many of
them using model checking for formalizing web service compositions [11, 13]. These approaches
focus on formalizing web service communications by state transition system in order to check
deadlock or LTL properties.
The paper [14] is aimed at enabling markup and automated reasoning technology to de-
scribe, simulate, compose and verify compositions of Web services. It defines the semantics for
a relevant subset of DAML-S in terms of a first-order logical language. With the semantics,
1The B notation does not support the Real type, we thus use Integer as a Money type
FORMALIZING AND CHECKING WEB SERVICE DISCOVERY MODELS USING B 85
MACHINE WS Requester
SEES Types
VARIABLES
availabilityR,
maxResTimeR, reliabilityR
. . .
INVARIANT
availabilityR ∈ AVAILABILITY ∧
maxResTimeR ∈ INT ∧
reliabilityR ∈ RELIABILITY
. . .
INITIALISATION
. . .
OPERATIONS
taxAmount ←− calcul Tax (
typeOfGoods ,quantity) =
PRE
typeOfGoods ∈ GOODS ∧
quantity ∈ INT ∧ quantity > 0
THEN
taxAmount :∈ MONEY
END ;
serviceQuality =
BEGIN
availabilityR := 98‖
maxResTimeR := 10‖
reliabilityR := 98 . . .
END
END
(a) Web service requester
REFINEMENT WS Provider
SEES Types
REFINES WS Requester
VARIABLES
taxOf , availabilityP ,
maxResTimeP , reliabilityP
...
INVARIANT
taxOf ∈ GOODS −→ MONEY ∧
availabilityP ∈ AVAILABILITY ∧
maxResTimeP ∈ INT ∧
reliabilityP ∈ RELIABILITY ∧
availabilityR ≤ availabilityP ∧
maxResTimeR ≥ maxResTimeP ∧
reliabilityR ≤ reliabilityP
...
INITIALISATION
...
OPERATIONS
taxAmount ←− calcul Tax (
typeOfGoods ,quantity) =
PRE
typeOfGoods ∈ GOODS ∧
quantity ∈ INT ∧ quantity > 0
THEN
taxAmount :=
taxOf (typeOfGoods) ∗ quantity
END ;
serviceQuality =
BEGIN
availabilityP := 99‖
maxResTimeP := 8‖
reliabilityP := 98...
END
END
(b) Web service provider
Hình 4.5. Formalizing web service discovery model of Tax system by B
86 TRUONG NINH THUAN, TRINH THANH BINH, VAN HIEU VU
they encode service descriptions in a Petri Net formalism and provide decision procedures for
Web service simulation, verification and composition.
Wang et al [17] present an idea about describing, verifying and developing Web Service
using the B-method. This work transforms the BPEL4WS documents based on WSDL into
the B machine models, and then uses the more rigorous and well-developed verification theory,
concept and supported tools to guarantee the validity of Web services and their composition.
The paper [15] proposes an approach based on DAML-S for semantic matching of Web
Service capabilities. They show how service capabilities are presented in the Profile section
of a DAML-S description and how a semantic match between advertisements and requests is
performed. However, this paper consider only the matching between inputs and ouputs of web
services but do not consider the conformance of precondition, effect as well as non-functional
properties of web services. Another paper concerns the connection between semantic webs and
formal methods presented in [9]. This work focuses on building a Semantic Web (RDF/DAML)
environment for supporting, extending and integrating many different formalisms.
6. CONCLUSION
Transformation techniques between different languages are useful and important not only
for checking Web ontology through software modeling languages and tools, but also for check-
ing and analysing complex software design models [8].
In this paper, we make a link between formal methods and SOA by presenting an approach
to formalize and check web service discovery models using B. Based on charateristics of B
specification which can be used to model a software system at different levels of abstraction,
we formalize requirements of web service requester desired in a high abstraction level and
capability of service provided in a lower abstraction level. The different abstraction levels in
the B method are developped in a consistent and incremental way and are guaranteed by
proof obligations between levels. The matching between two sides of web service discovery
models thus can be analyzed by using B provers which prove automatically proof obligations
generated.
The contribution of this paper can be used in early analysis of SOA applications by building
a B formal model. Alternatively, it can be also applied to check the matching of capabilities
between service requesters and service providers by extracting their capabilities. In the future,
we will consider to formalize the sending and receiving security aspects into WSD models in
order to apply the approach in a high security web service system.
REFERENCES
[1] 
[2] 
[3] 
[4] OWL-S: Semantic Markup for Web Services. 
[5] 
FORMALIZING AND CHECKING WEB SERVICE DISCOVERY MODELS USING B 87
[6] L. Bocchi and P. Ciancarini, On the impact of formal methods in the SOA, Electr. Notes Theor.
Comput. Sci. 160 (2006) 113–126.
[7] Clearsy, B4free, Available at  2004.
[8] J. S. Dong, From semantic web to expressive software specifications: a modeling languages spec-
trum, ICSE’06: Proceedings of the 28th International Conference on Software engineering,
ACM (2006) 1063–1064.
[9] J. S. Dong, J. Sun, and H. Wang, Semantic web for extending and linking formalisms, FME ’02:
Proceedings of the International Symposium of Formal Methods Europe, Springer-Verlag,
(2002) 587–606.
[10] M. G. Hinchey and J. P. Bowen, Applications of Formal Methods, Prentice Hall, 1995.
[11] R. Kazhamiakin, M. Pistore, and L. Santuari, Analysis of communication models in web service
compositions, WWW’06: Proceedings of the 15th international conference on World Wide
Web, ACM (2006) 267–276.
[12] B.-C. Ltd, B-Toolkit User’s Manual, Oxford (UK), 1996, Release 3.2.
[13] S. Nakajima, Model-checking of safety and security aspects in web service flows,
ICWE’04:International conference on Web Engineering (2004) 488–501.
[14] S. Narayanan and S. A. McIlraith, Simulation, verification and automated composition of web
services,WWW’02: Proceedings of the 11th International Conference on World Wide Web,
ACM (2002) 77–88.
[15] M. Paolucci, T. Kawamura, T. R. Payne, and K. P. Sycara, Semantic matching of web services
capabilities, ISWC’02: Proceedings of the First International Semantic Web Conference,
Springer-Verlag (2002) 333–347.
[16] S. Ran, A model for web services discovery with QoS, ACM SIGecom Exchange 4 1 (2003)
1–10.
[17] S. Wang, J. Wan, and X. Yang, Describing, verifying and developing web service using the
B-method, NWESP’06: Proceedings of the International Conference on Next Generation
Web Services Practices, IEEE Computer Society (2006) 11–16.
Received on February 2 - 2012