AUTHOR(S): 

May Haidar, Hicham H. Hallal

TITLE

A Formal Hybrid Analysis Technique for Composite Web Services Verification

KEYWORDS

Static Analysis, Dynamic Analysis, Property Patterns, Web Services, Model Checking, Automata Models

ABSTRACT

In this work, we propose to develop an integrated formal framework where both static and dynamic analysis techniques complement each other in enhancing the verification process of an existing web services based application. The proposed framework consists of three components. A Library of Property Patterns, which we intend to build on existing work and compile a library and a classification of web services properties (patterns and antipatterns). These would include BPEL4WS and WISCI requirements in the form of property patterns which can be instantiated in different contexts and for different purposes like verifying correctness, security, and performance related issues. The property library will be based on an easy to use template that depicts mainly the type, formal model, and example of a property. The second component is the development of Static Analysis Techniques that include direct code inspection, abstraction based techniques, and model based techniques. The third component is the development of dynamic analysis techniques that include extracting behavioral models of applications from observed executions and verifying them (mainly using model checking) against behavioral properties. These properties specify defects that cannot be detected using static analysis techniques. We elaborate in this paper the formal approach used to extract an automata based model of a web service composition from execution traces that are observed and collected using a monitoring tool. We also outline the components of a prototype to realize the proposed approaches for static analysis, modeling, and dynamic verification of the applications under test. In this paper we present the initial implementation of the dynamic approach.

Cite this paper

May Haidar, Hicham H. Hallal. (2017) A Formal Hybrid Analysis Technique for Composite Web Services Verification. International Journal of Internet of Things and Web Services, 2, 26-34