Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics | Formal Methods in System Design Skip to main content
Springer Nature Link
Log in

Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Process algebras are convenient formalisms to develop specifications stepwise. This can be done with the help of partially defined states in a specification. When refining the specification, new transitions are added to partially defined states. At every step, it is verified with the help of special preorders, refinement relations, that the step leads towards a desired goal. This approach has already been introduced in the case, where the verification is based on weak bisimulation equivalence. We show in this article that refinement relations can also be developed in decorated trace semantics. Moreover, the intuitive picture seems to be simpler in trace-based than in bisimulation-based semantics. The algorithms to compute the new refinement relations are exponential in the worst case, but behave quite well in practical cases.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. L. Aceto and M.C.B. Hennessy, “Adding action refinement to a finite process algebra,” Inform. and Comput., Vol. 115, pp. 204–269, 1994.

    Article  Google Scholar 

  2. A. Aho, J. Hopcroft, and J. Ullman, The Design and Analysis of Computer Algorithms., Addison-Wesley, 1974.

  3. R.-J. Back and J. von Wright, Refinement Calculus, A Systematic Introduction, Springer, 1998.

  4. J. Bergstra, J. Klop, and E.-R. Olderog, “Failure Semantics with fair abstraction,” CWI Report CS-8609, Centre for Mathematics and Computer Science, Amsterdam, The Netherlands, 1986.

  5. J. Bergstra, J. Klop, and E.-R. Olderog, “Failures without chaos: A new process semantics for fair abstraction,” in M. Wirsing (Eds.), Formal Description of Programming Concepts -III, IFIP, Elsevier Science Publishers B.V., 1987, pp. 77–101.

  6. T. Bolognesi and E. Brinksma, “Introduction to the ISO spesification language LOTOS,” Computer Networks and ISDN Systems, Vol. 14, pp. 25–59 1987.

    Article  Google Scholar 

  7. T. Bolognesi and M. Caneve, “Incremental development of a tool for equivalence verification,” Protocol Specification, Testing and Verification, VIII, 1988.

  8. T. Bolognesi and S. Smolka, “Fundamental results for the verification of observational equivalence,” in H. Rudin and C.H. West (Eds.), Protocol Specification, Testing and Verification VII, 1987, pp. 165–179.

  9. E. Brinksma, “A theory for the derivation of tests,” The Formal Description Technique LOTOS, North-Holland, 1989, pp. 235–247.

  10. U. Celikkan and R. Cleaveland, “Computing diagnostic information for incorrect processes,” Protocol Specification, Testing and Verification, XII, Elsevier Science Publishers B.V.(Noerth-Holland), IFIP, 1992, pp. 263–277.

  11. U. Celikkan and R. Cleaveland, “Generating diagnostic information for behavioral preorders,” Distributed Computing, Vol. 9, No. 2, pp. 61–75, 1995.

    Article  Google Scholar 

  12. R. Cleaveland and M. Hennessy, “Testing equivalence as a bisimulation equivalence,” in Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag, 1990, pp. 11–23.

  13. R. Cleaveland and M. Hennessy, “Testing Equivalence as a Bisimulation Equivalence,” Formal Aspects of Computing, Vol. 5, pp. 1–20, 1993.

    Article  Google Scholar 

  14. R. Cleaveland, J. Parrow, and B. Steffen, “The concurrency workbench,” in Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag, 1990, pp. 24–37.

  15. R. Cleaveland and B. Steffen, “A preorder for partial process specifications,” in J. Baeten and J. Klop (Eds.), Theories of Concurrency: Unification and Extension, CONCUR ‘90, Lecture Notes in Computer Science 458, Springer-Verlag, 1990, pp. 141–151.

  16. J.P. Courtiat and D.E. Saidouni, “Action refinement in lotos,” Formal Description Techniques, V(C-10), Elsevier Science Publishing, 1993 IFIP.

  17. E.W. Dijkstra, Discipline of Programming, Prentice Hall, Englewood Cliffs, New Jersey, 1976.

    Google Scholar 

  18. J. Fernandez, “An implementation of an efficient algorithm for bisimulation equivalence,” Science of Computer Programming, Vol. 13, pp. 219–236, 1989/90.

    Article  Google Scholar 

  19. J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu, “CADP (Caesar/aldebaran development package) a protocol validation and verification toolbox,” in R. Alur and T.A. Henzinger (Eds.), Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA), Lecture Notes in Computer Science, Berlin, Springer Verlag, August 1996, pp. 437-440.

  20. M. Hennessy, “Acceptance trees,” Journal of the ACM, Vol. 32, No. 4, pp. 896–928, 1985.

    Article  Google Scholar 

  21. J. Hopcroft and J. Ullman, Introduction to Automata Theory, Languages and Computation, Addison-Wesley, 1979.

  22. P. Kanellakis and S. Smolka, “CCSexpressions, finite state processes and three problems of equivalence,” in Proceedings of ACM Symposium on Principles of Distributed Computing, 1983.

  23. T. Karvi, “Partially defined lotos specifications and their refinement relations,” Dissertation, University of Helsinki, Department of Computer Science, Series of Publications A, Report A-2000-5. Available in ps-form at http://ethesis.helsinki.fi/julkaisut/mat/tieto/vk/karvi.

  24. R. Mateescu, “Formal description and analysis of a bounded retransmission protocol,” in Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, June 17–19 Maribor, Slovenia, 1996, pp. 98–113.

  25. R. Milner, Communication and Concurrency, Prentice Hall, 1989.

  26. R. Paige and R. Tarjan, “Three partition refinement algorithms,” SIAM J. Computing, Vol. 16, No. 6, pp. 973–989, 1987.

    Article  Google Scholar 

  27. A. Valmari, “The weakest deadlock-preserving congruence,” Information Processing Letters Vol. 53, pp. 341–346, 1995.

    Article  Google Scholar 

  28. A. Valmari and M. Tienari, “An improved failures equivalence for finite-state systems with a reduction algorithm,” in 11th International IFIP WG6.1 Symposium on Protocol Specification, Testing and Verification, Stockholm, 1991, pp. 1–16.

  29. A. Valmari and M.Tienari, “Compositional failure-based semantic models for basic LOTOS,” Formal Aspects of Computing, Vol. 7, pp. 440–468, 1995.

    Article  Google Scholar 

  30. D. Walker, “Bisimulation and divergence,” Information and Computation, Vol. 85, pp. 202–241, 1990.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Helsinki, P.O. box 26, FIN-00014, Helsinki, Finland

    T. Karvi & M. Tienari

  2. Department of Computer Science, University of Helsinki, currently with Intel Corporation, Hillsboro, Oregon, USA

    R. Kaivola

Authors
  1. T. Karvi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. Tienari
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. R. Kaivola
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Karvi, T., Tienari, M. & Kaivola, R. Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics. Form Method Syst Des 26, 293–317 (2005). https://doi.org/10.1007/s10703-005-1631-9

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-005-1631-9

Keywords

Search

Navigation