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. © 2012 Springer-Verlag.
CITATION STYLE
Rossi, S. (2012). Model checking adaptive multilevel service compositions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6921 LNCS, pp. 106–124). https://doi.org/10.1007/978-3-642-27269-1_7
Mendeley helps you to discover research relevant for your work.