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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Alpern and F.B. Schneider, Defining Liveness, Information Processing Letters, 21(4), 181–185,1985
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
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
D. Bjørner, H. Langmaack, C.A.R. Hoare, ProCoS I Final Deliverable, ProCoS Technical Report ID/DTH db 13/1, January 1993
G. Boriello, Formalized Timing Diagrams, in Proc. European Conference on Design Automation, Belgium, 1992
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
J.R. Burch et al., Symbolic Model Checking: 1020 States and Beyond, in Proc. of the Fifth Annual Logic in Computer Science, 1990
E.M. Clarke et al., Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications, ACM TOPLAS 8, 1986
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
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
E.C.R. Helmer, Predicative Programming, Comm. ACM 27 (2), 1984
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
C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, London, 1985
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
ITU-TS, ITU-TS Recommendation Z.120: Message Sequence Chart (MCS), ITU-TS, Geneva, 1994
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
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
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
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
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
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.
S. Kleuker, Incremental Development of Deadlock-Free Communicating Systems, in E. Brinksma (ed.), Proc. of TACAS'97, LNCS 1217 (Springer), 1997
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
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
Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems-Safety, Springer, 1995
S. Mauw, M.A. Reniers, An algebraic semantics of Basic Message Sequence Charts, The computer journal, 37(4), 1994
E.-R. Olderog, Towards a Design Calculus for Communicating Programs, LNCS 527 (Springer), p. 61–77, 1991
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.
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
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
M.Y. Vardi, An Automata-Theoretic Approach to Linear Temporal Logic, in F. Moller, G. Birteistle (eds.), Logics for concurrency,, LNCS 1043 (Springer), 1996
J. Zwiers, Compositionality, Concurrency and Partial Correctness-Proof Theories for Networks of Processes and their Relationship, LNCS 321 (Springer), 1989
Author information
Authors and Affiliations
Editor information
Rights 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