Verification of Web Services Modeled as Finite State Machines

Currently, model based development of web services is being actively researched for its usefulness in developing a system. Various techniques like EPC, petrinet, process algebra, CPN and UML have been proposed for web service modeling. FSM is found appropriate to model Business requirements because a business process on execution moves forward from one state to other. We have shown uses of FSM (Finite State Machine) based models in development of web services [1], also have developed a tool HUMSAT to model service specification in FSM and to generate executable codes in BPEL and WSDL. However, automated code generation depends on correct specification of models as an improperly specified model leads to errors and bugs in resultant code. Hence model checking plays an important role in eliminating the flaws at design phase itself. In this paper, we propose a technique for model verification that identifies structural flaws e.g. unreachability, deadlock and temporal inconsistencies. Further, HUMSAT is augmented with the model verification features.