Model Checking & Verification Of Web Services Protocol using Uppaal & Tla
By: Channa, Asadullah 10MSIT11 Supervisor - Dr. Muhammad Saleem Vighio.
Material type:
BookPublisher: Nawabshah: QUEST, 2014Online resources: Click here to access online
| Item type | Current location | Call number | Status | Date due | Barcode | Item holds |
|---|---|---|---|---|---|---|
Thesis and Dissertation
|
Research Section | Available | MP/07-60 |
ABSTRACT
The behavior of systems (protocols, car engines, embedded systems, and so on) is
usually provided in specifications which give details on how systems work and what
properties they should satisfy. These specifications are written informally using
natural languages, state transition tables, and data flow diagrams. However, these
informal specifications are usually prone to errors, imprecise, ambiguous and
sometimes lack important details. Therefore, it is very important that such
specifications must be verified before using them in real-life scenarios. In this thesis,
we present formal verification of web service business activity protocol described
informally. The said protocol is specified by the Microsoft and the IBM Companies
to be used in modern business applications. The formal verification is provided using
the model checkers UPPAAL and TLC. We verify the key properties of the protocol
in order to ensure the correct behavior. Furthermore, based on our analysis we
present a comparative study of the verification techniques: UPPAAL and TLA+ by
considering quantitative and qualitative parameters.(Ms Theses)
Click on an image to view it in the image viewer
There are no comments for this item.