Software quality is an important matter in many application areas of modern software engineering. A key to achieve it is the usage of formal analysis. Formal stands for the specification of software using formal models and the analysis of these models using formal methods with respect to certain properties.
In case of service oriented architectures where different services are composed together, often need to be assembled or changed on-the-fly. This creates huge challenges to guarantee the desired quality of such composed services. Here ‘quality’ refers to both the functional and non-functional requirements. Analysis of such services also must be done with a specified time thereby imposing timing constraints. Different quality assurance method works by transforming a composition into an analysis model which captures the semantics of the composition. But such techniques are time consuming and difficult to apply in on-the-fly composition. The central approach of this project is to use templates which capture the known compositional patterns and verify those using Hoare-style proof calculus to prove their correctness.
Fig. 1 illustrates our approach. Templates are defined as workflow descriptions with service placeholders, which are replaced by concrete services during instantiation. Every template specification contains pre- and post-conditions which are used to verify the correctness of the templates. Once a template has been proven correct, we only need to prove certain side conditions for the instantiations and can then conclude their correctness.