{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:12:58Z","timestamp":1725664378361},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540585558"},{"type":"electronic","value":"9783540490319"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58555-9_89","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:36:45Z","timestamp":1330274205000},"page":"83-92","source":"Crossref","is-referenced-by-count":1,"title":["Verification techniques for LOTOS"],"prefix":"10.1007","author":[{"given":"U.","family":"Martin","sequence":"first","affiliation":[]},{"given":"M.","family":"Thomas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"J.C. Bicarregui, Algorithm Refinement with Read and Write Frames, Proceeding of Formal Methods Europe '93 Symposium, Odense, April 1993, LNCS 670, Springer-Verlag.","DOI":"10.1007\/BFb0024644"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"D.W. Bustard, M.T.Norris, R.A. Orr, and A.C. Winstanley, An Exercise in Formalizing the Description of a Concurrent System, Software practice and experience, 22 (1992).","DOI":"10.1002\/spe.4380221204"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"P. Curran and K.J. Norrie, An approach to verifying concurrent systems \u2014 a medical information bus (MIB) case study, in Proceedings of the 5th annual IEEE symposium on computer-based medical systems, Durham, North Carolina, 74\u201383, 1992.","DOI":"10.1109\/CBMS.1992.244961"},{"key":"7_CR4","unstructured":"A. J. J. Dick and J. R. Kalmus, ERIL Users manual, Rutherford Appleton Laboratory 1988, RAL-88-055"},{"key":"7_CR5","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1093\/comjnl\/34.1.16","volume":"34","author":"A. J. J. Dick","year":"1991","unstructured":"A. J. J. Dick and P. Watson, Order-Sorted Term Rewriting, Computer Journal, 34 (1991) 16\u201319","journal-title":"Computer Journal"},{"key":"7_CR6","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1111\/1467-8659.1220123","volume":"12","author":"D.A. Duce","year":"1993","unstructured":"D.A. Duce and F. Paterno, A Formal Specification of a Graphics System in the Framework of the Computer Graphics Reference Model, Computer Graphics Forum, 12 (1993) 123\u2013130.","journal-title":"Computer Graphics Forum"},{"key":"7_CR7","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1111\/1467-8659.1110017","volume":"11","author":"D.A. Duce","year":"1992","unstructured":"D.A. Duce and L. Damnjanovic, Formal Specification in the Revision of GKS: An Illustrative Example, Computer Graphics Forum, 11 (1992) 17\u201330","journal-title":"Computer Graphics Forum"},{"key":"7_CR8","doi-asserted-by":"crossref","first-page":"544","DOI":"10.1007\/3-540-56610-4_88","volume":"668","author":"C. Kirkwood","year":"1993","unstructured":"C. Kirkwood, Automating (Specification = Implementation) using Equational Reasoning and LOTOS, in TAPSOFT'93: Theory and Practice of Software Development, Springer Lecture Notes in Computer Science 668, (1993) 544\u2013558","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"7_CR9","unstructured":"C. Kirkwood, Verification of LOTOS Specifications Using Term Rewriting Techniques, Ph.D. thesis, University of Glasgow, 1994."},{"key":"7_CR10","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0304-3975(89)90020-0","volume":"67","author":"U. Martin","year":"1989","unstructured":"U. Martin, A geometrical approach to multiset orderings, Theoretical computer Science 67 (1989) 37\u201354","journal-title":"Theoretical computer Science"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"U. Martin, Linear interpretations by counting patterns, in Springer Lecture Notes in Computer Science 690, 5th International Conference on Rewriting Techniques and Applications, Montreal, 1993","DOI":"10.1007\/3-540-56868-9_31"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"U. H. Martin and T. Nipkow, Ordered Rewriting and Confluence in Proceedings of the 10th International conference on Computer Aided Deduction, Lecture Notes in Computer Science 607, 1990.","DOI":"10.1007\/3-540-52885-7_100"},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/0747-7171(92)90007-Q","volume":"13","author":"U. H. Martin","year":"1992","unstructured":"U. H. Martin and M. K. F. Lai, Some experiments with a completion theorem prover, Journal of Symbolic Computation (1992) 13, 81\u2013100","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Ursula Martin and Elizabeth Scott, The order types of termination orderings on terms, strings and multisets, in Proceedings of the Eighth IEEE Conference on Logic in Computer Science, Montreal, 1993","DOI":"10.1109\/LICS.1993.287573"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"U.H. Martin and J. Wing (editors), Proceedings of the First International Workshop on Larch, Workshops in Computer Science Series, Springer Verlag, 1993.","DOI":"10.1007\/978-1-4471-3558-6"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"B.M. Matthews, MERILL: An Equational Reasoning System in Standard ML: A User Guide RAL technical report, RAL-93-026, April 1993.","DOI":"10.1007\/3-540-56868-9_34"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"B.M. Matthews, MERILL: An Equational Reasoning System in Standard ML, in Springer Lecture Notes in Computer Science 690, 5th International Conference on Rewriting Techniques and Applications, Montreal, June 1993","DOI":"10.1007\/3-540-56868-9_34"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"E.A.Scott, An automated proof of the correctness of compiling specification, in M. Nivat, T. Rus, G. Scollo editors, Proceedings of AMAST: Algebraic Methodology and Software Technology, Workshops in Computing, Springer Verlag, 1993.","DOI":"10.1007\/978-1-4471-3227-1_42"},{"key":"7_CR19","first-page":"3","volume":"1","author":"M. Thomas","year":"1994","unstructured":"M. Thomas, The Story of Therac-25 in LOTOS, High Integrity Systems Journal, 1, (1994) 3\u201315","journal-title":"High Integrity Systems Journal"},{"key":"7_CR20","first-page":"35","volume":"1","author":"M. Thomas","year":"1994","unstructured":"M. Thomas, A Proof of Incorrectness using the LP Theorem Prover: The Editing Problem in the Therac-25. High Integrity Systems Journal, 1 (1994) 35\u201348","journal-title":"High Integrity Systems Journal"},{"key":"7_CR21","first-page":"37","volume-title":"Formal Description Techniques","author":"M. Thomas","year":"1993","unstructured":"M. Thomas, A Translator Tool for ASN.1 into LOTOS, in M. Diaz, Ro. Groz, editors, Formal Description Techniques, V. pp. 37\u201352, Elsevier Science Publishers B.V. (North-Holland), 1993."},{"key":"7_CR22","unstructured":"M. Thomas, A Note on An Exercise in the Formalization of a Concurrent System, manuscript, 1993."},{"key":"7_CR23","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0304-3975(93)90241-K","volume":"112","author":"M. Thomas","year":"1993","unstructured":"M. Thomas and P. Watson, Solving Divergence in Knuth-Bendix Completion by Enriching Signatures. Theoretical Computer Science, 112, (1993) 145\u2013185","journal-title":"Theoretical Computer Science"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"M. Thomas and P. Watson, Solving Divergence in Knuth-Bendix Completion by Enriching Signatures. Extended abstract, in M. Nivat, T. Rus, G. Scollo editors, Proceedings of AMAST: Algebraic Methodology and Software Technology, Workshops in Computing, Springer Verlag, 1993.","DOI":"10.1016\/0304-3975(93)90241-K"},{"key":"7_CR25","unstructured":"D. Craigen, S. Gerhart and T. Ralston, An International Survey of Industrial Formal Methods. Report NISTGCR 93\/626 from US Department of Commerce, National Institute for Standards and Technology, March 1993."},{"key":"7_CR26","unstructured":"ISO [ISO:8807] Information Processing Systems: Open Systems Interconnection: LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, 1988."},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"D. Kapur and H. Zhang, RRL: Rewrite Rule Laboratory User's Manual, 1987.","DOI":"10.1007\/3-540-16780-3_140"},{"key":"7_CR28","unstructured":"H. Lin, PAM: A Process Algebra Manipulator, University of Sussex, Computer Science Technical Report, 2\/91."},{"key":"7_CR29","unstructured":"J. Quemada, S. Pav\u00f3n, A. Fernandez, Transforming LOTOS specifications with LOLA \u2014 The Parameterised Expansion, in Formal Description Techniques I, K. Turner (ed.), North-Holland, 1988."}],"container-title":["Lecture Notes in Computer Science","FME '94: Industrial Benefit of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58555-9_89.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:23:11Z","timestamp":1605648191000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58555-9_89"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540585558","9783540490319"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-58555-9_89","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}