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)