Consistent graphical specification of distributed systems

  • Franz Huber
  • Bernhard Schätz
  • Geralf Einert
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


The widely accepted possible benefits of formal methods on the one hand and their minor use compared to informal or graphical description techniques on the other hand have repeatedly lead to the claim that formal methods should be put to a more indirect or transparent use. We show how such an indirect approach can be incorporated in a CASE tool prototype by basing it upon formally defined hierarchical description techniques. We demonstrate the immediate benefits by introducing consistency notions gained from the formalization. Additionally, we show how the formalization can be used to apply automated property validation. Finally, we discuss some further techniques that could be based on the underlying formalization.


Model Check Consistency Condition Output Port Consistency Check Transition Relation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A. Biere. Eine Methode zur,μ-Kalkül-Modellprüfung. Slides for the AKFM from 23.05.96, GI/ITG-Fachgespräch ‘Formale Beschreibungstechniken für verteilte Systeme” (in German), 1996.Google Scholar
  2. [2]
    M. Broy, C. Dendorfer, F. Dederichs, M. Fuchs, T. Gritzner, and R. Weber. The Design of Distributed Systems-An Introduction to FOCUS. Technical Report TUM-19225, Technische Universität München, 1992.Google Scholar
  3. [3]
    M. Fuchs and M. Mendler. Functional Semantics for Delta-Delay VHDL based on Focus. In: C. Delgado Kloos and P. Breuer (eds.). Formal Semantics for VHDL, Kluwer Academic Publishers, 1994, Chapter 1, pp. 9–38.Google Scholar
  4. [4]
    R. Grosu, C. Klein, B. Rumpe, and M. Broy. State Transition Diagrams. Technical Report TUM-19630, Technische Universität München, 1996.Google Scholar
  5. [5]
    D. Harel and A. Naamad. The Statemate Semantics of Statecharts. IEEE Transactions of Software Engineering Methods, 1996.Google Scholar
  6. [6]
    F. Huber, B. Schätz, A. Schmidt, and K. Spies. AutoFocus-A Tool for Distributed System Specification. In: B. Jonsson and J. Parrow (eds.). Proceedings FTRTFT'96. Lecture Notes in Computer Science 1135, Springer, 1996, pp. 476-470.Google Scholar
  7. [7]
    International Telecommunication Union. Message Sequence Charts, 1996. ITU-T Recommendation Z.129. Geneva, 1996.Google Scholar
  8. [8]
    M. P. Jones. Introduction to Gofer 2.20. Technical Report, Yale University, 1991.Google Scholar
  9. [9]
    J.-L. Lions et al. Ariane S Flight 501 Failure. ESA Press Release 33–96, Paris, 1996.Google Scholar
  10. [10]
    D. Park. Finitness is μ-inefble. Theoretical Computer Science 3(2), 1976, pp. 173–181.Google Scholar
  11. [11]
    F. Regensburger. HOLCF. Higher Order Logic of Computable Functions. In: T. Schubert, P. Windley, and J. Alves-Foss (eds.). Higher Order Logic Theorem Proving and Its Application (HOL95), 1995, pp. 293–307.Google Scholar
  12. [12]
    R. Sandner and Olaf Müller. Theorem Prover Support for the Refinement of Stream Processing Functions. Proc. 3rd Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97). Lecture Notes in Computer Sience Vol. 1217. Springer, 1997, pp. 351-365.Google Scholar
  13. [13]
    B. Schätz, H. Hußmann, and M. Broy. Graphical Development of Consistent System Specifications. In: J. Woodcock, M.-C. Gaudel (eds.). FME' 96. Lecture Notes in Computer Science Vol. 1051, Springer, 1996, pp. 248–267.Google Scholar
  14. [14]
    B. Schatz and K. Spies. Formale Syntax zur logischen Kernsprache der Focus-Entwicklungsmethodik. Technial Report TUM-I9529, Technische Universität München, 1995.Google Scholar
  15. [15]
    D. von Oheimb. Datentypspezifikationen in HOLCF. Master's Thesis, Technische Universität München, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Franz Huber
    • 1
  • Bernhard Schätz
    • 1
  • Geralf Einert
    • 1
  1. 1.Fakultät für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations