Service compositions proposed by subproject B2 as an OTF configurator have to fulfill various functional requirements. Due to the complexity of their analysis, it cannot be done during the service selection. Our subproject supports subproject B2 by providing feedback on properties like protocol compatibility, deadlock freedom, and adherence to semantic requirements, modeled by pre- and postconditions.
Services within the composition can belong to different functional layers, such as the application, platform, infrastructure, etc., which reflects the SaaS, PaaS and IaaS service forms originating from the cloud computing. These layers need to be flexibly woven to allow transformation and compositional analysis of the given service composition.
We develop a modular model transformation process based on the model weaving technique. After independently transforming individual layers, we connect their analysis models by means of glue code obtained from the weaving model. This way we can (re-)use model transformation definitions as well as their results for individual layers.
The spectrum of analysis models we use includes process algebras like CSP (Communicating Sequential Processes) supported by tools like FDR2 (Failures-Divergence Refinement), process specifications like Promela for the SPIN model checker, and probabilistic reactive modules supported by PRISM (Probabilistic Symbolic Model Checker). For domain specific modeling and reasoning, we employ ontologies and SMT (Satisfiability Modulo Theories) solvers like Z3.