Model checking adaptive service compositions

• We present a technique for verifying security and correctness of multilevel service compositions.
• We define modal μ-calculus formulae interpreted over service configurations.
• We use filters as prescriptions of behaviour, i.e., coercions to prevent service misbehaviour.
• We devise a model checking algorithm for adaptive service compositions.
• We study a case-study of a federated login system.

We present a logic-based verification framework for multilevel security and transactional correctness of service oriented architectures. The framework is targeted at the analysis of data confidentiality, enforced by non-interference, and of service responsiveness, captured by a notion of compliance that implies deadlock and livelock freedom. We isolate a class of modal μ-calculus formulae, interpreted over service configurations, that characterise configurations satisfying the properties of interest. We then investigate an adaptation technique based on the use of coercion filters to block any action that might potentially break security or transactional correctness. Based on the above, we devise a model checking algorithm for adaptive service compositions which automatically synthesises the maximal (most expressive/permissive) filter enforcing the desired security and correctness properties.