Channa, Asadullah 10MSIT11 Supervisor - Dr. Muhammad Saleem Vighio creator text Nawabshah QUEST 2014 monographic 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) https://tinyurl.com/2hx8k9j6 https://tinyurl.com/2hx8k9j6