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. The results of this analysis may have stochastic characteristics.
Composed systems generally consist of several services – e.g. web services – that are selected and combined at runtime (On-The-Fly). This implies that efficiency is of particular interest during the analysis. Part of the composition are infrastructural models, represented as services themselves, to incorporate information about the runtime environment. The central approach of the project is the usage of model transformations to transform the initial composition into various formal models, which can be handled by existing analysis tools. The formalisms of choice depend on the properties which are subject to a specific analysis, e.g. integrated specification languages concerning correctness properties, queueing networks concerning performance analysis oder Markov chains concerning reliability. The model transformation has to be specific for each chosen formalism.
The analysis of a composed system assumes, that every single service, that is part of the composition, already provides an analysis result for its properties. The reuse of these existing results contributes to the reduction of the state space of the analysis model. However, it is possible that information about analysis results for single services is either incomplete or, to a certain degree, unreliable. The analysis methods have to consider the (potential) partiality of this information when making a conclusion regarding the properties the whole composition.
This project ist part of the subproject „B3“ of the Collaborative Research Center 901 (Sonderforschungsbereich 901) of the Deutsche Forschungsgemeinschaft DFG. A particular focus in this context is the analysis of models at runtime – On-The-Fly –, because the exact composition is known only just before deployment. The usage of parameterised service specification languages which support multiple views (subproject „B1“) poses an additional challenge. By starting with selected aspects and analysing functional and non-functional requirements separately, in the course of the project all specified requirements should be covered.