Verification of Communication Protocols in Web Services: Model-Checking Service Compositions

CHAPTER 9

CONCLUSIONS AND OUTLOOK

In this book we have addressed the intriguing issues related to model checking and verification of BPEL specifications. The research has been motivated by the necessity for a wider use of formal methods to enhance the safety and reliability of software systems. The research has also been driven by the lack of robustness in loosely coupled SOA-based applications.

As observed previously, model checking is a rigorous technique wherein all possible behaviors of a system are scrutinized exhaustively to determine a problem. Consequently, model checking is expected to identify all issues in a system. However, there are significant time and memory requirements in model-checking a system [6]. Therefore, the scope of model checking has hitherto been limited to critical systems where reliability is excessively important. Nevertheless, with our ever-increasing dependence on software in everyday life (e.g., traffic signals, elevators), skipping model checking amounts to risking millions of human lives.

In Chapters 5 and 6 we propose novel techniques to reduce the time and memory requirements for model checking. The reduction in memory requirements envisioned for model checking is realized by storing states as the difference from the preceding on nearest state. The time reduction is attributed to generating the reachability graph for each module of a hierarchical model in parallel. The techniques proposed offer better results for larger models that correspond ...