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

CHAPTER 6

TIME-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODEL CHECKING

In Chapter 5 we identified the significance of formal methods for service compositions as well as their associated massive time and memory costs. Considering the ubiquity of software systems in our daily life, Chapter 5 vouched for the wider use of formal methods to warrant their correctness and usability. The sequential and tree models were described to pursue this inducement by reducing the memory costs involved in model checking, a widely used formal method. However, as with any memory-reduction technique, the models were found to have an associated time overhead.

In this chapter we seek to reduce the aforementioned delay by introducing concurrency into the paradigm of model checking. Contemporary model-checking languages offer different levels of abstraction by defining a notion of hierarchy wherein a system is modeled as a set of interdependent modules. The reduction in time offered is attributed to the concurrent exploration of all such modules in a hierarchical model and exposing the outcome using special data structures. This allows the modules to interact with each other and resolve their dependencies when generating the state space. Experiments report a time reduction of 86% in generating the first 25,000 markings. Furthermore, the reduction offered increases as more markings are generated. Compared to recent solutions, which depend on the existence of stubborn sets and/or symmetry in the state space, ...