Advertisement

Functional Specification of Time Sensitive Communicating Systems

  • Manfred Broy
Conference paper
Part of the NATO ASI Series book series (volume 88)

Abstract

A formal model and a logical framework for the functional specification of time sensitive communicating systems and their components is outlined. The specification method is modular w.r.t. sequential composition, parallel composition, and communication feedback. Nondeterminism is included by underspecification. The application of the specification method to timed communicating functions is demonstrated. Abstractions from time are studied. In particular a rational is given for the chosen concepts of the functional specification technique. The relationship between system models based on nondeterminism and system models based on explicit time notions is investigated. Forms of reasoning are considered The alternating bit protocol is used as a running example.

Keywords

Safety Property Sequential Composition Parallel Composition Input Stream Concrete State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Brock, Ackermann 81 ]
    J.D. Brock, W.B. Ackermann: Scenarios: A model of nondeterminate computation. In: I Diaz, I. Ramos (eds): Lecture Notes in Computer Science 107, Springer 1981,225–259Google Scholar
  2. [Broy 83]
    M. Broy: Applicative real time programming. Information Processing 83, IHP World Congress, Paris 1983, North Holland Publ. Company 1983,259–264Google Scholar
  3. [Broy 85]
    M. Broy: Specification and top down design of distributed systems. In: H. Ehrig et al. (eds.): Formal Methods and Software Development. Lecture Notes in Computer Science 186, Springer 1985,4–28, Revised version in JCSS 34:2/3,1987,236–264Google Scholar
  4. [Broy 86]
    M. Broy: A theory for nondeterminism, parallelism, communication and concurrency. Habilitation, Fakultät für Mathematik und Informatik der Technischen Universität München, 1982, Revised version in: Theoretical Computer Science 45 (1986) 1–61CrossRefMATHMathSciNetGoogle Scholar
  5. [Broy 87a]
    M. Broy: Semantics of finite or infinite networks of communicating agents. Distributed Computing 2 (1987), 13–31CrossRefMATHGoogle Scholar
  6. [Broy 87b]
    M. Broy: Predicative specification for functional programs describing communicating networks. Information Processing Letters 25 (1987) 93–101CrossRefMATHMathSciNetGoogle Scholar
  7. [Dybier, Sander 88]
    P. Dybier, H. Sander: A functional programming approach to the specification and verification of concurrent systems. Chalmers University of Technology and University of Göteborg, Department of Computer Sciences 1988Google Scholar
  8. [Jonsson 88]
    B. Jonsson: A fully abstract trace model for dataflow networks. 16th POPL 1989,155 –165Google Scholar
  9. [Kahn,MacQueen77]
    G. Kahn and D. MacQueen, Coroutines and networks of processes, Proc. IFIP World Congress 1977, 993–998Google Scholar
  10. [Kok 87]
    J.N. Kok: A fully abstract semantics for data flow networks. Proc. PARLE, Lecture Notes in Computer Science 259, Berlin-Heidelberg-New York: Springer 1987,214–219Google Scholar
  11. [Lamport 83]
    L. Lamport: Specifying concurrent program modules. ACM Toplas 5:2, April 1983,190–222CrossRefMATHGoogle Scholar
  12. [Park 80]
    D. Park: On the semantics of fair parallelism. In: D. Björner (ed.): Abstract Software Specification. Lecture Notes in Computer Science 86, Berlin-Heidelberg-New York: Springer 1980, 504–526Google Scholar
  13. [Schieder 91]
    B. Schieder: Private Communications, 1991Google Scholar
  14. [Schneider 87]
    F.B. Schneider: Decomposing properties into safety and liveness using predicate logic. Cornell University, Department of Computer Science, Technical Report 87–874, October 1987Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Manfred Broy
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchen 2Germany

Personalised recommendations