|
This document includes various qualitative analyses for verifying properties of service implementations with respect to their formal specifications. They are briefly described and put in a broader perspective in this document. The goal of WP3 is to develop qualitative analyses for verifying properties of service implementations with respect to their formal specifications. This document selects a subset of the 34 original contributions described in detail in the companion Deliverable D3.a. With the help of the selected contributions, we identify analysis challenges that arise from the WP8 case studies and the WP2 core calculi. The selected contributions show how these challenges can be tackled and provide a foundation for future theme-oriented deliverables across WP2, WP3, and WP8. The current approaches address several issues as confidentiality, integrity, non-interference, access control and trust management including specific issues related to SOA as service composition. The analysis scenarios and threat models discussed range from the common Dolev-Yao model to ad hoc scenarios as mobile wireless systems one, where attackers have to obey to domain specific restrictions. On a more practical side, also specific techniques for access control to services have been designed and successfully implemented. The problem of resource usage of mobile services has been addressed at two distinct linguistic levels (process calculi and programming languages) and by exploiting different analysis techniques (type systems, flow logic and model checking). Five original contributions is the result of this research activity: type systems for termination of processes, flow logic for resource access control, type systems for confining movements of data and processes, type systems for composition of incomplete software components and model checking properties of workflow processes. The research comprises the analysis of a wide spectrum of techniques suitable for the description and analysis of the behavioural properties of services. Temporal logics, and modal logics (which allow to mix temporal and other structural/spatial operators), are two of the promising techniques, which have been investigated in several directions. Flow analysis, and type based analysis are representatives of a different approach more aimed to the static enforcement of correctness of distributed services rather than to the dynamic verification of them. Graph Transformation Systems are a flexible formalism for the specification of the operational behaviour of complex systems. The goal of WP3 is to develop qualitative analyses for verifying properties of service implementations with respect to their formal specifications.
This deliverable directly builds on the deliverable D3.b. That deliverable described a number of challenging scenarios on the automotive case study and on linguistic primitives, together with some initial work aimed at attacking them. The present deliverable D3.c reports on the continuation of this strand of work, where we go more deeply into the challenges and we tackle some new ones.
Altogether, 19 original contributions (resulting in 21 papers) have been collected as part of the activity reported in the deliverable. They are briefly described and put in a broader perspective in this document. We refer to the references given in the "Relevant Sensoria Publications and Reports" section for full details of the contributions. The goal of WP3 is to develop qualitative analyses for verifying properties of service implementations with respect to their formal specifications. This deliverable presents the tools that have been developed to carry out the analysis of the techniques in an automated, or semi-automated, way.
We present four different tools, all developed during the Sensoria project exploiting new techniques and calculi from the Sensoria project itself. |
