[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Consistent graphical specification of distributed systems

  • Conference paper
  • First Online:
FME '97: Industrial Applications and Strengthened Foundations of Formal Methods (FME 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1313))

Included in the following conference series:

Abstract

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.

This work was carried out within the sub-project A6 of the “Sonderforschungsbereich 342 (Werkzeuge und Methoden für die Nutzung paralleler Rechnerarchitekturen)" and the SysLab project, s onsored by the German Research Community (DFG) under the Leibniz program and by Siemens-Nixdorf.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

Bibliography

  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. 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. 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. 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. D. Harel and A. Naamad. The Statemate Semantics of Statecharts. IEEE Transactions of Software Engineering Methods, 1996.

    Google Scholar 

  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. International Telecommunication Union. Message Sequence Charts, 1996. ITU-T Recommendation Z.129. Geneva, 1996.

    Google Scholar 

  8. M. P. Jones. Introduction to Gofer 2.20. Technical Report, Yale University, 1991.

    Google Scholar 

  9. J.-L. Lions et al. Ariane S Flight 501 Failure. ESA Press Release 33–96, Paris, 1996.

    Google Scholar 

  10. D. Park. Finitness is μ-inefble. Theoretical Computer Science 3(2), 1976, pp. 173–181.

    Google Scholar 

  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. 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. 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. 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. D. von Oheimb. Datentypspezifikationen in HOLCF. Master's Thesis, Technische Universität München, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität München, Arcisstraße 21, 80333, München, Germany

    Franz Huber, Bernhard Schätz & Geralf Einert

Authors
  1. Franz Huber
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard Schätz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Geralf Einert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Fitzgerald Cliff B. Jones Peter Lucas

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huber, F., Schätz, B., Einert, G. (1997). Consistent graphical specification of distributed systems. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-63533-5_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63533-8

  • Online ISBN: 978-3-540-69593-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation