Formal Methods in the Era of Service-Oriented Design

The adoption of services on the architectural side has been rather prompt, sometimes turning a pre-existing offer of component-like software into a coarse or fine granular offer of services, in a quick SOA adaptation, and more recently along the lines proposed by the Service Component Architecture (SCA). On the contrary, service-oriented computing (the operational side of the SO-* paradigm) is not as easily producible from preexisting systems that were not conceived for this kind of deep-black box provision. The behavioural side of service engineering is still lagging behind the maturity of the mere architectural perspective because it is intrinsically more difficult to convert post factum. The realm of consistency and compliance is the home turf of formal methods; but which formal methods are adequate to support seamlessly this very large scale and heterogeneous transition to the era of services en masse? Delegation and hiding are the primary commandments of thinking in services; but what is truly required is automatic, efficient, powerful machine-readable support in a world that systematically shields internal details, and this for all the questions that concern eg. service selection and composition from a behavioural point of view. How it is built is not important, how it functions and how to use the service are here in the center of the attention.