000			01509nam a22001097a 4500
999			_c56276 _d56273
100			_aChanna, Asadullah _a10MSIT11 _aSupervisor - Dr. Muhammad Saleem Vighio
245			_aModel Checking & Verification Of Web Services Protocol using Uppaal & Tla
260			_aNawabshah: _bQUEST, _c2014.
500			_aABSTRACT 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)
856			_uhttps://tinyurl.com/2hx8k9j6
942			_cTHESIS