{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:21:08Z","timestamp":1725664868825},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635338"},{"type":"electronic","value":"9783540695936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63533-5_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:29:43Z","timestamp":1330298983000},"page":"102-121","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing requirements for distributed systems with trace diagrams"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Kleuker","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"issue":"4","key":"6_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F.B. Schneider, Defining Liveness, Information Processing Letters, 21(4), 181\u2013185,1985","journal-title":"Information Processing Letters"},{"key":"6_CR2","unstructured":"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"},{"key":"6_CR3","unstructured":"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"},{"key":"6_CR4","unstructured":"D. Bj\u00f8rner, H. Langmaack, C.A.R. Hoare, ProCoS I Final Deliverable, ProCoS Technical Report ID\/DTH db 13\/1, January 1993"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"G. Boriello, Formalized Timing Diagrams, in Proc. European Conference on Design Automation, Belgium, 1992","DOI":"10.1109\/EDAC.1992.205958"},{"key":"6_CR6","unstructured":"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"},{"key":"6_CR7","unstructured":"J.R. Burch et al., Symbolic Model Checking: 1020 States and Beyond, in Proc. of the Fifth Annual Logic in Computer Science, 1990"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"E.M. Clarke et al., Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications, ACM TOPLAS 8, 1986","DOI":"10.1145\/5397.5399"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/3-540-61648-9_51"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/192218.192226"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"E.C.R. Helmer, Predicative Programming, Comm. ACM 27 (2), 1984","DOI":"10.1145\/69610.357988"},{"key":"6_CR12","volume-title":"Mathematical Logic and Programming Languages","author":"C.A.R. Hoare","year":"1985","unstructured":"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"},{"key":"6_CR13","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, London, 1985"},{"key":"6_CR14","unstructured":"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"},{"key":"6_CR15","unstructured":"ITU-TS, ITU-TS Recommendation Z.120: Message Sequence Chart (MCS), ITU-TS, Geneva, 1994"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Jifeng He, C.A.R. Hoare, M. Fr\u00e4nzle, M. M\u00fcller-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","DOI":"10.1007\/3-540-58468-4_171"},{"key":"6_CR17","unstructured":"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"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/BFb0035388"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/3-540-60973-3_103"},{"key":"6_CR20","unstructured":"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"},{"key":"6_CR21","volume-title":"Formal Description Techniques IX","author":"S. Kleuker","year":"1996","unstructured":"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."},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"S. Kleuker, Incremental Development of Deadlock-Free Communicating Systems, in E. Brinksma (ed.), Proc. of TACAS'97, LNCS 1217 (Springer), 1997","DOI":"10.1007\/BFb0035396"},{"key":"6_CR23","unstructured":"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"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/BF01211870"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems-Safety, Springer, 1995","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"S. Mauw, M.A. Reniers, An algebraic semantics of Basic Message Sequence Charts, The computer journal, 37(4), 1994","DOI":"10.1093\/comjnl\/37.4.269"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"E.-R. Olderog, Towards a Design Calculus for Communicating Programs, LNCS 527 (Springer), p. 61\u201377, 1991","DOI":"10.1007\/3-540-54430-5_81"},{"key":"6_CR28","unstructured":"E.-R. Olderog, S. R\u00f6ssig, 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."},{"key":"6_CR29","unstructured":"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"},{"key":"6_CR30","unstructured":"R. Schl\u00f6r, W. Damm, Specification and Verification of System Level Hardware Designs using Timing Diagrams, in Proc. The European Conference on Design Automation, Paris, France, 1993"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi, An Automata-Theoretic Approach to Linear Temporal Logic, in F. Moller, G. Birteistle (eds.), Logics for concurrency,, LNCS 1043 (Springer), 1996","DOI":"10.1007\/3-540-60915-6_6"},{"key":"6_CR32","unstructured":"J. Zwiers, Compositionality, Concurrency and Partial Correctness-Proof Theories for Networks of Processes and their Relationship, LNCS 321 (Springer), 1989"}],"container-title":["Lecture Notes in Computer Science","FME '97: Industrial Applications and Strengthened Foundations of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63533-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:55Z","timestamp":1605647935000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}