Operating guidelines have been introduced to characterize all controllers for a given service S. A controller of S is a service that interacts with S without deadlocking. An operating guideline of S can be used to decide whether S refines another service. It is a special-purpose structure to describe the behavior of service S from the perspective of its controllers rather than from the perspective of S.

This paper provides a more conceptual understanding of operating guidelines from the perspective of a traditional concurrency semantics: a trace-based semantics. As benefits, we get an easier characterization of service refinement, and prove that this is a fully abstract precongruence.


  1. 1.
    Boreale, M., De Nicola, R., Pugliese, R.: Trace and testing equivalence on asynchronous processes. Inf. Comput. 172(2), 139–164 (2002)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)MathSciNetCrossRefGoogle Scholar
  3. 3.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC / SIGSOFT FSE 2001, pp. 109–120 (2001)Google Scholar
  4. 4.
    de Boer, F.S., Kok, J.N., Palamidessi, C., Rutten, J.J.M.M.: The failure of failures in a paradigm for asynchronous communication. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 111–126. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  5. 5.
    De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Fournet, C., Hoare, T., Rajamani, S.K., Rehof, J.: Stuck-Free Conformance. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 242–254. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Laneve, C., Padovani, L.: The must preorder revisited. In: Caires, L., Li, L. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Lohmann, N., Massuthe, P., Wolf, K.: Operating guidelines for finite-state services. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 321–341. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    Lohmann, N., Wolf, K.: Compact representations and efficient algorithms for operating guidelines. Fundam. Inform. (2010) (accepted for publication in January 2010)Google Scholar
  10. 10.
    Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)zbMATHGoogle Scholar
  11. 11.
    Milner, R.: Fully abstract models of typed lambda-calculi. Theor. Comput. Sci. 4(1), 1–22 (1977)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Englewood Cliffs (1989)zbMATHGoogle Scholar
  13. 13.
    Mooij, A.J., Voorhoeve, M.: Proof techniques for adapter generation. In: Bruni, R., Wolf, K. (eds.) WS-FM 2008. LNCS, vol. 5387, pp. 207–223. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Papazoglou, M.P.: Web Services: Principles and Technology. Pearson, London (2007)Google Scholar
  15. 15.
    Stahl, C., Massuthe, P., Bretschneider, J.: Deciding substitutability of services with operating guidelines. In: Jensen, K., van der Aalst, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency II. LNCS, vol. 5460, pp. 172–191. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Vogler, W.: Modular Construction and Partial Order Semantics of Petri Nets. LNCS, vol. 625. Springer, Heidelberg (1992)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Christian Stahl
    • 1
  • Walter Vogler
    • 2
  1. 1.Department of Mathematics and Computer ScienceTechnische Universiteit EindhovenThe Netherlands
  2. 2.Institut für InformatikUniversität AugsburgGermany

Personalised recommendations