Combining Aspects of Reactive Systems

  • Leonid Kof
  • Bernhard Schätz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)


For reactive systems, a large collection of formal models has been developed. While the formal relationship between those models is often carefully analyzed, the methodical implications for selecting or constructing appropriate models for specific application domains are rarely addressed. We classify and compare different specification methods for distributed systems concerning communication, behavior, and causality. We discuss the implications of these dimensions, especially concerning the combination of their properties.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Owicki, S., Gries, D.: An Axiomatic Proof Technique for Parallel Programs. Acta Informatica 14 (1976)Google Scholar
  2. 2.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs (1985)zbMATHGoogle Scholar
  3. 3.
    Milner, R.: Communication and Concurrency. Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  4. 4.
    Chandy, K.M., Misra, J.: Parallel Program Design - A Foundation, 2nd edn. Addison-Wesley, Reading (1989)Google Scholar
  5. 5.
    Berry, G.: The Esterel v5 Language Primer. Technical report, INRIA (2000), (accessed August 19 2002)
  6. 6.
    Broy, M., Stølen, K.: Specification and Development of Interactive Systems: FOCUS on Streams, Interfaces, and Refinement. Texts and Monographs in Computer Science. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  7. 7.
    von der Beeck, M.: Comparison of Statecharts Variants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863. Springer, Heidelberg (1994)Google Scholar
  8. 8.
    van Glabbeek, R.J.H.: Comparative concurrency semantics and refinement of actions. Technical Report 109, Centrum voor Wiskunden en Informatica, CWI Tracts (1996)Google Scholar
  9. 9.
    Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits. ACM Distinguished Dissertations. The MIT Press (1989)Google Scholar
  10. 10.
    Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design: An International Journal 15, 7–48 (1999)CrossRefGoogle Scholar
  11. 11.
    Schätz, B.: Ein methodischer Übergang von asynchronen zu synchronen Systemen. PhD thesis, Technische Universität München (1998)Google Scholar
  12. 12.
    Bergstra, J.A., Ponse, A., Smolka, S.A.: Handbook of Process Algebra. Elsevier, Amsterdam (2001)zbMATHGoogle Scholar
  13. 13.
    Lynch, N., Tuttle, M.: An Introduction to Input/Output Automata. CWI Quarterly 2, 219–246 (1989)zbMATHMathSciNetGoogle Scholar
  14. 14.
    Josephs, M.B.: Receptive process theory. Acta Informatica 29, 17–31 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Lamport, L.: Verification and Specification of Concurrent Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 347–374. Springer, Heidelberg (1994)Google Scholar
  16. 16.
    Shields, M.W.: Semantics of Parallelism. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  17. 17.
    Scholz, P.: Design of reactive Systgems and their Distributed Implementaion with Statecharts. PhD thesis, Technische Universität München (1998)Google Scholar
  18. 18.
    Parrow, J.: Fairness properties in process algebra with applications in communication protocol verification. PhD thesis, Uppsala University (1985)Google Scholar
  19. 19.
    Davis, J., Schneider, S.: An Introduction to Timed CSP. PRG- 75, PRG Programming Research Group Oxford (1989)Google Scholar
  20. 20.
    Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems 16, 1543–1571 (1994)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Leonid Kof
    • 1
  • Bernhard Schätz
    • 1
  1. 1.Fakultät für InformatikTechnische Universität MünchenGarching bei MünchenGermany

Personalised recommendations