Model Checking Adaptive Multilevel Service Compositions

In this paper we present a logic-based technique for verifying both security and correctness properties of multilevel service compositions. We define modal μ-calculus formulae interpreted over service configurations. Our formulae characterize those compositions which satisfy a non-interference property and are compliant, i.e., are both deadlock and livelock free. Moreover, we use filters as prescriptions of behavior (coercions to prevent service misbehavior) and we devise a model checking algorithm for adaptive service compositions which automatically synthesizes an adapting filter.