Skip to main content
SpringerLink
Log in

Formalizing requirements for distributed systems with trace diagrams

  • Conference paper
  • First Online:
Book cover 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:

  • 248 Accesses

Abstract

Graphical formalisms can be useful to bridge the gap between informal requirements written by application experts and formal requirements used by formal methods experts. Trace diagrams are a new graphical formalism that was developed during several case studies in the telecommunications area to express relations between allowed and disallowed sequences of communications. This paper introduces the graphical and textual syntax as well as its formal semantics. It is shown that trace diagrams can easily be extended at the informal and formal level to serve other applications.

This research was supported by the Leibniz Programme of the Deutsche Forschungsgemeinschaft (DFG) under grant No. 0198/1-1

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.

References

  1. B. Alpern and F.B. Schneider, Defining Liveness, Information Processing Letters, 21(4), 181–185,1985

    MathSciNet  Google Scholar 

  2. C. Antoine, B. Le Goff, Timing Diagrams for Writing and Checking Logical and Behavioural Properties of Integrated Systems, in P. Prinetti, P Camurati (eds.), Correct Hardware Design Methodologies, Elsevier Science Publishers, 1992

    Google Scholar 

  3. J. Bohn, S. Rossig. On automatic and interactive design of communicating systems, in E. Brinksma, W. R. Cleaveland, K. G. Larsen, T Margaria, and B. Steffen (eds.), Proceedings of TACAS'95, LNCS 1019 (Springer), 1995

    Google Scholar 

  4. D. Bjørner, H. Langmaack, C.A.R. Hoare, ProCoS I Final Deliverable, ProCoS Technical Report ID/DTH db 13/1, January 1993

    Google Scholar 

  5. G. Boriello, Formalized Timing Diagrams, in Proc. European Conference on Design Automation, Belgium, 1992

    Google Scholar 

  6. M. Broy, F. Dederichs, C. Dendorfer, M. Fuchs, T.F. Gritzner, R. Weber, The Design of Distributed Systems-An Introduction to FOCUS-Revised Version, technical report TUM-19202-2, Technical University of Munich, 1993

    Google Scholar 

  7. J.R. Burch et al., Symbolic Model Checking: 1020 States and Beyond, in Proc. of the Fifth Annual Logic in Computer Science, 1990

    Google Scholar 

  8. E.M. Clarke et al., Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications, ACM TOPLAS 8, 1986

    Google Scholar 

  9. C. Dietz, Graphical Formalization of Real-Time Requirements, in B. Jonsson, J. Parrow (eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems '96, LNCS 1135 (Springer), 1996

    Google Scholar 

  10. L.K. Dillon, G. Kutty, L.E. Moser, P.M. Melliar-Smith, Y.S. Ramakrishna, A Graphical Interval Logic for Specifying Concurrent Systems, ACM Transactions on Software Engineering and Methodology, vol. 3, no. 2, April 1994

    Google Scholar 

  11. E.C.R. Helmer, Predicative Programming, Comm. ACM 27 (2), 1984

    Google Scholar 

  12. C.A.R. Hoare, Programs are Predicates, in C.A.R. Hoare, J.C. Shepherdson (Eds.), Mathematical Logic and Programming Languages, Prentice-Hall, London, 1985

    Google Scholar 

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

    Google Scholar 

  14. ISO, revised text of CD 10731, information technology-Open Systems Interconnection-conventions for the definition of OSI services, technical report, ISO/OEC JTC 1/SC 21 N 6341, ISO, 1991

    Google Scholar 

  15. ITU-TS, ITU-TS Recommendation Z.120: Message Sequence Chart (MCS), ITU-TS, Geneva, 1994

    Google Scholar 

  16. Jifeng He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.-R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn, H. Rischel, Provably Correct Systems, in H. Langmaack, W.P. de Roever, Y. Vytopil (eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems '94, LNCS 863 (Springer), 1994

    Google Scholar 

  17. J.G. Henriksen et al., MONA: Monadic Second-Order Logic in Practice, in E. Brinksma, W. R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen (eds.), Proceedings of TACAS'95, LNCS 1019 (Springer), 1995

    Google Scholar 

  18. P. Kelb, T. Margaria, M. Mendler, C. Gsottberger, Mosel: A Flexible Toolset for Monadic Second-Order Logic, in E. Brinksma (ed.), Proc. of TACAS'97, LNCS 1217 (Springer), 1997

    Google Scholar 

  19. S. Kleuker, H. Tjabben, The Incremental Development of Correct Specifications for Distributed Systems, in M.-C. Gaudel, J. Woodcock (eds.), Formal Methods Europe '96, LNCS 1051 (Springer), 1996

    Google Scholar 

  20. S. Kleuker, H. Tjabben, A Formal Approach to the Development of Reliable MultiUser Multimedia Applications, Philips Research Laboratories Aachen, Technical Report, 1168/96, ftp://ftp.informatik.uni-Odenburg.de/pub/procos/cocon/mumu.ps.gz

    Google Scholar 

  21. S. Kleuker. Using Formal Methods in the Development of Protocols for Multi-User Multimedia Systems, in R. Gotzhein, J. Bredereke (eds.), Formal Description Techniques IX, Chapman & Hall, London, 1996.

    Google Scholar 

  22. S. Kleuker, Incremental Development of Deadlock-Free Communicating Systems, in E. Brinksma (ed.), Proc. of TACAS'97, LNCS 1217 (Springer), 1997

    Google Scholar 

  23. B. Krieg-Bruckner, J. Peleska, E.-R. Olderog, D. Balzer, A. Baer, UniForM: Universal Formal Methods Workbench, in Statusseminar des BMBF, Softwaretechnologie, Berlin, March 1996

    Google Scholar 

  24. L. Lamport, How to Write a Long Formula, technical research report, Digital Equipment Corporation, in http://www.research.digital.com/SRC/proofs/proofs.html, 1994

    Google Scholar 

  25. Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems-Safety, Springer, 1995

    Google Scholar 

  26. S. Mauw, M.A. Reniers, An algebraic semantics of Basic Message Sequence Charts, The computer journal, 37(4), 1994

    Google Scholar 

  27. E.-R. Olderog, Towards a Design Calculus for Communicating Programs, LNCS 527 (Springer), p. 61–77, 1991

    Google Scholar 

  28. E.-R. Olderog, S. Rössig, J. Sander, M. Schenke, ProCoS at Oldenburg: The Interface between Specification Language and OCCAM-like Programming Language. Technical Report Bericht 3/92, Univ. Oldenburg, Fachbereich Informatik, 1992.

    Google Scholar 

  29. Y.S. Ramakrishna, P.M. Melliar-Smith, L.E. Moser, L.K. Dillon, G. Kutty, Really Visual Temporal Reasoning, in Proc. 14th RTSS, Raliegh-Durham, IEEE Press, 1993

    Google Scholar 

  30. R. Schlör, W. Damm, Specification and Verification of System Level Hardware Designs using Timing Diagrams, in Proc. The European Conference on Design Automation, Paris, France, 1993

    Google Scholar 

  31. M.Y. Vardi, An Automata-Theoretic Approach to Linear Temporal Logic, in F. Moller, G. Birteistle (eds.), Logics for concurrency,, LNCS 1043 (Springer), 1996

    Google Scholar 

  32. J. Zwiers, Compositionality, Concurrency and Partial Correctness-Proof Theories for Networks of Processes and their Relationship, LNCS 321 (Springer), 1989

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oldenburg - FB Informatik, P.O. Box 2503, 26111, Oldenburg, Germany

    Stephan Kleuker

Authors
  1. Stephan Kleuker
    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

Kleuker, S. (1997). Formalizing requirements for distributed systems with trace diagrams. 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_6

Download citation

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

  • 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