Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Specification Diagrams for Actor Systems

  • Published:
Higher-Order and Symbolic Computation

Abstract

Specification diagrams (SD's) are a novel form of graphical notation for specifying open distributed object systems. The design goal is to define notation for specifying message-passing behavior that is expressive, intuitively understandable, and that has formal semantic underpinnings. The notation generalizes informal notations such as UML's Sequence Diagrams and broadens their applicability to later in the design cycle. Specification diagrams differ from existing actor and process algebra presentations in that they are not executable per se; instead, like logics, they are inherently more biased toward specification. In this paper we rigorously define the language syntax and semantics and give examples that show the expressiveness of the language, how properties of specifications may be asserted diagrammatically, and how it is possible to reason rigorously and modularly about specification diagrams.

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
$34.99 /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 excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi, M. and Lamport, L. The existence of refinement mappings. Theor. Comput. Sci., 82(2) (1991) 253–284.

    Google Scholar 

  2. Agha, G. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, 1986.

    Google Scholar 

  3. Agha, G., Mason, I.A., Smith, S.F., and Talcott, C.L. A foundation for actor computation. Journal of Functional Programming, 7 (1997) 1–72.

    Google Scholar 

  4. Allwein, G. and Barwise, J. (Eds.). Logical Reasoning With Diagrams. Oxford University Press, Oxford, 1996.

    Google Scholar 

  5. Attardi, G. and Hewitt, C. Specifying and proving properites of guardians for distributed systems, 1978.

  6. Back, R.J.R. Refinement calculus II: Parallel and reactive systems. In Stepwise Refinement of Distributed Systems, J.W. de Bakker, W.P. de Roever, and G. Rozenberg (Eds.), vol. 430 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

  7. Back, R.J.R. and Sere, K. Stepwise refinement of parallel algorithms. Science of Computer Programming, 13 (1989) 133–180.

    Google Scholar 

  8. Baker, H.G. and Hewitt, C. Laws for communicating parallel processes. In IFIP Congress, IFIP, Aug. 1977, pp. 987–992.

  9. Bardohl, R. Genged-a generic graphical editor for visual languages. In 1998 IEEE Symposium on Visual Languages, Sept. 1998.

  10. Bolognesi, T. and Brinksma, E. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14 (1987) 25–59.

    Google Scholar 

  11. Breu, R., Hinkel, U., Hofmann, C., Klein, C., Paech, B., Rumpe, B., and Thurner, V. Towards a formalization of the unified modeling language. In ECOOP '97, vol. 1241 of Lecture Notes in Computer Science, Springer-Verlag, 1997, pp. 344–365.

  12. Clinger, W.D. Foundations of Actor Semantics. PhD thesis, MIT, 1981. MIT Artificial Intelligence Laboratory AI-TR-633.

  13. R.S. Corporation. UML Notation Guide, version 1.1. Sept. 1997. Obtained From http://www. rational.com.

  14. Denker, G. DTL+: A Distributed Temporal Logic Supporting Several Communication Principles. Technical Report, SRI International, Computer Science Laboratory, 333 Ravenswood Ave, Menlo Park, CA 94025, 1998. To appear.

  15. Dijkstra, E. and Scholten, C. Predicate Calculus and Program Semantics, vol. 14 of Texts and Monographs in Computer Science. Springer-Verlag, 1990.

  16. Duarte, C.H.C. A proof-theoretic approach to the design of object-based mobility. In Formal Methods for Open Object-Based Distributed Systems, H. Bowman and J. Derrick (Eds.), Chapman & Hall, 1997, Vol. 2, pp. 37–53.

  17. Ellsberger, J., Hogrefe, D., and Sarma, A. SDL-Formal Object-Oriented Language for Communication Systems. Prentice Hall, 1997.

  18. Eschbach, R., Glässer, U., Gotzhein, R., and Prinz, A. On the formal semantics of sdl-2000: A compilation approach based on an abstract sdl machine. In InternationalWorkshop on Abstract State Machines (ASM'2000), vol. 1912 of Lecture Notes in Computer Science, Springer-Verlag, 2000.

  19. Felleisen, M. and Friedman, D.P. A syntactic theory of sequential state. Theoretical Computer Science, 69 (1989) 243–287.

    Google Scholar 

  20. Frølund, S. Coordinated Distributed Objects: An Actor Based Approach to Synchronization. MIT Press, 1996.

  21. Greif, I. Semantics of communicating parallel processes. Technical Report 154, MIT, Project MAC, 1975.

  22. Gunter, E., Muscholl, A., and Peled, D. Compositional message sequence charts. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), T. Margaria and W. Yi (Eds.), vol. 2031 of Lecture Notes in Computer Science, Springer, Apr. 2001, pp. 496–511.

  23. Harel, D. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3) (1987) 231–274.

    Google Scholar 

  24. Hewitt, C. Viewing control structures as patterns of passing messages. Journal of Artificial Intelligence, 8(3) (1977) 323–364.

    Google Scholar 

  25. Hewitt, C., Bishop, P., and Steiger, R. A universal modular actor formalism for artificial intelligence. In Proceedings of 1973 International Joint Conference on Artificial Intelligence, Aug. 1973, pp. 235–245.

  26. Hoare, C.A.R. Communicating Sequential Processes. Prentice-Hall, 1985.

  27. Message Sequence Chart (MSC). ITU-T Recommendation Z.120, International Telecommunications Union, Nov. 1996.

  28. ITU-T. Revised Recommendation Z. 100 Specification and Description Language (SDL), May 1994. Addendum 1996.

  29. Lamport, L. The temporal logic of actions. ACM TOPLAS, 16(3) (1994) 872–923.

    Google Scholar 

  30. Manna, Z. and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Verlag, 1992.

  31. Mason, I.A. and Talcott, C.L. Actor languages: Their syntax, semantics, translation, and equivalence. Theoretical Computer Science, 220 (1999) 409–467.

    Google Scholar 

  32. Milner, R. A Calculus of Communicating Systems, vol. 92 of Lecture Notes in Computer Science. Springer Verlag, 1980.

  33. Milner, R. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, May 1999.

  34. Nelson, G. A generalization of dijkstra's calculus. TOPLAS, 11 (1987) 517–561.

    Google Scholar 

  35. Roscoe, A. The Theory and Practice of Concurrency. Prentice-Hall, 1998.

  36. Rumbaugh, J., Jacobson, I., and Booch, G. Unified Modeling Language Reference Manual. Addison-Wesley, 1998.

  37. Saraswat, V.A. Concurrent Constraint Programming. ACM Doctoral Dissertation Awards: Logic Programming. The MIT Press, Cambridge, MA, 1993.

    Google Scholar 

  38. Smith, S. On specification diagrams for actor systems. In Proceedings of the Second Workshop on Higher-Order Techniques in Semantics, C.T.A. Gordon and A. Pitts (Eds.), Electronic Notes in Theoretical Computer Science. Elsevier, 1998. http://www.elsevier.nl/locate/entcs/volume10.html.

  39. Smith, S. and Talcott, C. Specification diagrams for actor systems. In Formal Methods in Object-Oriented Distributed Systems (FMOODS). Kluwer Academic Publishers, 1999.

  40. Talcott, C.L. Interaction semantics for components of distributed systems. In 1st IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems, FMOODS'96, E. Najm and J.-B. Stefani (Eds.), 1996. Proceedings published in 1997 by Chapman & Hall.

  41. Talcott, C.L. Composable semantic models for actor theories. Higher-Order and Symbolic Computation, 11(3) (1998) 281–343.

    Google Scholar 

  42. Talcott, C.L. Actor theories in rewriting logic, 1999. submitted for publication.

  43. Wirsing, M. Algebraic specification. In Handbook of Theoretical Computer Science, J. van Leeuwen (Ed.), North-Holland, Amsterdam, 1990, Vol. B, pp. 675–788.

    Google Scholar 

  44. Wirsing, M. and Knapp, A. A formal approach to object oriented software engineering. In Proc. 1st Intl. Workshop on Rewriting Logic and Its Applications, J. Meseguer (Ed.), number 4 in Electronic Notes in Theoretical Computer Science, Elsevier, 1996. URL: http://www.elsevier.nl/locate/entcs/ volume4.html.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The Johns Hopkins University, Baltimore, MD, 21218, USA

    Scott F. Smith

  2. SRI International, 333 Ravenswood Ave., Menlo Park, CA, 94025-3493, USA

    Carolyn L. Talcott

Authors
  1. Scott F. Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carolyn L. Talcott
    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

Smith, S.F., Talcott, C.L. Specification Diagrams for Actor Systems. Higher-Order and Symbolic Computation 15, 301–348 (2002). https://doi.org/10.1023/A:1022934504959

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1022934504959

Search

Navigation