01509nam a22001097a 4500 56276 56273 Channa, Asadullah 10MSIT11 Supervisor - Dr. Muhammad Saleem Vighio Model Checking & Verification Of Web Services Protocol using Uppaal & Tla Nawabshah: QUEST, 2014. 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 THESIS 0 0 0 0 RESEARCH RESEARCH 2016-12-01 MP/07-60 2016-12-01 2016-12-01 THESIS