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

CHAPTER 7

GENERATING HIERARCHICAL MODELS BY IDENTIFYING STRUCTURAL SIMILARITIES

Model checking requires formulating a formal representation of a system prior to verifying it. Considering the parallel components in a service composition, this translation often leads to an enormous increase in the size of the representation obtained, which eventually becomes a computational bottleneck in model-checking algorithms. Such a massive model is difficult to draw and impractical to analyze and maintain [9]. Consequently, it is prone to errors and omissions that impair the benefits of model checking. Furthermore, the lack of abstraction and classification in such voluminous formal models prevents a human modeler from developing a thorough understanding.

To obtain a more succinct representation with multiple levels of abstraction, any system needs to embrace the notion of hierarchy [2]. In a hierarchical setup, each system component is represented by a module wherein the module for a high-level component refers to its underlying components using their module name or reference. Apart from rendering an elegant, abstract, and expressive model, such a setup also makes it possible to avoid a state-space explosion by applying compositional model checking [8].

In this chapter we describe a decrease-and-conquer-based method for installing hierarchy into an otherwise “flat” model. This method involves determining structurally similar components in a flat model and creating a module for each of them. ...