Using Goals To Infer Formal Behavioral Models From Web Service Applications

We propose an integrated framework for the formal analysis of web services based applications involving both static and dynamic analysis techniques. The proposed framework consists of three main components: A library of patterns, representing both recommended and undesired services related properties along with an efficient classification of the compiled patterns according to their effect on the behavior of web services based applications; a set of static analysis techniques that use tools like code inspection, abstraction extraction, and model inference to detect property patterns in the source code of the applications under test; and a set of dynamic analysis techniques directly mainly to verify web services based applications against property patterns that cannot be detected using only the source code of applications. In this paper, we elaborate the work completed on the development of an approach to dynamic analysis of web services based applications, we describe the formal model used to depict the behavior of an application based on it observed execution traces, and we outline the workflow of a goal based inference approach to derive behavioral models.