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

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