O'Reilly logo

Verification of Communication Protocols in Web Services: Model-Checking Service Compositions by Peter Bertok, Zahir Tari, Kazi Sakib

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required