{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:44:05Z","timestamp":1725493445544},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664925"},{"type":"electronic","value":"9783540482420"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48242-3_7","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:28:09Z","timestamp":1184603289000},"page":"92-110","source":"Crossref","is-referenced-by-count":3,"title":["Animating TLA Specifications"],"prefix":"10.1007","author":[{"given":"Yassine","family":"Mokhtari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"7_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"81","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The Existence of Refinement Mappings. Theoretical Computer Science 81(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"M. Abadi and S. Merz. On TLA as as logic. in M. Broy (ed.): Deductive Program Design. Springer-Verlag, NATO ASI series F, 1996.","key":"7_CR2","DOI":"10.1007\/978-3-642-61455-2_14"},{"doi-asserted-by":"crossref","unstructured":"J.-R Abrial. The B-Book. Cambridge University Press, 1996.","key":"7_CR3","DOI":"10.1017\/CBO9780511624162"},{"unstructured":"B-core. B-Toolkit. User\u2019s Manual, Release 3.2. Technical Report, B-core, 1996","key":"7_CR4"},{"doi-asserted-by":"crossref","unstructured":"M. Baudinet. Temporal Logic Programming is Complete and Expressive. In Proc. ACM Conf. on Princinples of Programming Languages, pp. 267\u2013280 (1989)","key":"7_CR5","DOI":"10.1145\/75277.75301"},{"key":"7_CR6","first-page":"185","volume-title":"Proc. 8th Z Users Workshop (ZUM94), Workshops in Computing","author":"P. Breuer","year":"1994","unstructured":"P. Breuer and J. Bowen. Towards Correct Executable Semantics for Z. In J. Bowen and J. Hall, editors, Proc. 8th Z Users Workshop (ZUM94), Workshops in Computing, pages 185\u2013212. Cambridge, Springer-Verlag, Berlin, 1994."},{"unstructured":"http:\/\/www.cs.tut.fi\/laitos\/DisCo\/DisCo-english.fm.html","key":"7_CR7"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson and E.M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2 (1982), pages 241\u2013266.","journal-title":"Science of Computer Programming"},{"key":"7_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Executable Modal and Temporal Logics","author":"M. Fisher","year":"1993","unstructured":"M. Fisher and R. Owens. An introduction to Executable Modal and Temporal Logics. In Michael Fisher and Richards Owens editors, Executable Modal and Temporal Logics, volume 897 of Lecture Notes in Computer Science, pages 1\u201320, Springer-Verlag, 1993."},{"key":"7_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Executable Modal and Temporal Logics","author":"M. Fisher","year":"1993","unstructured":"M. Fisher. Concurrent METATEM\u2014The Language and its Applications. In Michael Fisher and Richards Owens editors, Executable Modal and Temporal Logics, volume 897 of Lecture Notes in Computer Science, Springer-Verlag, 1993."},{"issue":"5","key":"7_CR11","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1049\/sej.1992.0033","volume":"7","author":"N. E. Fuchs","year":"1992","unstructured":"N. E. Fuchs. Specifications are (preferably) executable. Software Engineering Journal, 7(5), pages 323\u2013334,1992","journal-title":"Software Engineering Journal"},{"key":"7_CR12","first-page":"3","volume":"XIII","author":"R. Gerth","year":"1995","unstructured":"R. Gerth, D. Peled, M. Vardi and P. Wolper Simple on-the-fly automatic verification of linear temporal logic PSTV, XIII, pages 3\u201318, 1995","journal-title":"Simple on-the-fly automatic verification of linear temporal logic PSTV"},{"key":"7_CR13","first-page":"109","volume":"XIII","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid and G. J. Holzmann On the verification of temporal properties PSTV, XIII, pages 109\u2013124, 1993","journal-title":"On the verification of temporal properties PSTV"},{"doi-asserted-by":"crossref","unstructured":"J. Goguen and G. Malcolm. Algebraic Semantics of Imperative Programs. MIT Press, 1997.","key":"7_CR14","DOI":"10.7551\/mitpress\/1188.001.0001"},{"unstructured":"A. Gravell. Executing Formal Specifications Need Not Be Harmful. Available on the WWW at URL http:\/\/dsse.ecs.soton.ac.uk\/amg\/papers.html .","key":"7_CR15"},{"doi-asserted-by":"crossref","unstructured":"C.A. Hoare. An Overview of Some Formal Methods for Program Design. IEEE Computer, pages 85\u201391, 1987.","key":"7_CR16","DOI":"10.1109\/MC.1987.1663697"},{"issue":"6","key":"7_CR17","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1049\/sej.1989.0045","volume":"4","author":"I. J. Hayes","year":"1989","unstructured":"I. J. Hayes and C. B. Jones Specifications are not (necessarily) executable. Software Engineering Journal,4(6), pages 320\u2013338,1989","journal-title":"Software Engineering Journal"},{"key":"7_CR18","volume-title":"EATCS Monographs on Theoretical Computer Science","author":"F. Kr\u00f6ger","year":"1987","unstructured":"F. Kr\u00f6ger Temporal Logic of Programs. EATCS Monographs on Theoretical Computer Science 8. Berlin, Springer-Verlag, 1987"},{"unstructured":"L. Lamport. The module structure of TLA+ Research Report 1996-002, Digital Equipment Corporation, Systems Research Center.","key":"7_CR19"},{"unstructured":"L. Lamport. The operators of TLA+ Research Report 1997-006a, Digital Equipment Corporation, Systems Research Center.","key":"7_CR20"},{"issue":"3","key":"7_CR21","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR22","volume-title":"Mathematical Logic and Hilbert\u2019s \u025b-Symbol","author":"A. C. Leisenring","year":"1969","unstructured":"A. C. Leisenring. Mathematical Logic and Hilbert\u2019s \u025b-Symbol. Gordon and Breach, New York, 1969."},{"key":"7_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems-Specifications","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli The Temporal Logic of Reactive and Concurrent Systems-Specifications New-York etc.: Springer-Verlag, 1992"},{"key":"7_CR24","series-title":"Lect Notes Comput Sci","first-page":"69","volume-title":"Executable Modal and Temporal Logics, IJCAI\u201993 Workshop","author":"S. Merz","year":"1993","unstructured":"S. Merz. Efficiently Executable Temporal Logic Programs. In Michael Fisher and Richards Owens editors, Executable Modal and Temporal Logics, IJCAI\u201993 Workshop, volume 897 of Lecture Notes in Computer Science, pages 69\u201385, France, 1993, Springer."},{"issue":"4","key":"7_CR25","doi-asserted-by":"crossref","first-page":"413ff","DOI":"10.1016\/0743-1066(92)90055-8","volume":"13","author":"M.A. Orgun","year":"1992","unstructured":"M.A. Orgun and W.W. Wadge. Towards a unified theory of intensional logic programming. Journal of Logic Programming 13(4), pp. 413ff (1992)","journal-title":"Journal of Logic Programming"},{"doi-asserted-by":"crossref","unstructured":"J. Rushby. Formal Methods and their Role in the Certification of Critical Systems. SRI Technical Report CSL-95-1, March 1995.","key":"7_CR26","DOI":"10.1007\/978-1-4471-0921-1_1"},{"doi-asserted-by":"crossref","unstructured":"L. Sterling, P. Ciancarini and T. Turnidge. On the animation of \u201cnot executable\u201d specifications by Prolog. International Journal of Software Engineering and Knowledge Engineering, 6(1):63\u201387.","key":"7_CR27","DOI":"10.1142\/S0218194096000041"},{"unstructured":"M. Utting. Animating Z: Interactivity, transparency and equivalence. Technical Report 94-40. Software Verification Research Center.","key":"7_CR28"},{"unstructured":"M. Vardi and P. Wolper An automata-theoretic approach to automatic program verification Proceedings on the First Symposium on Logic in Computer Science, pages 322\u2013331,1986","key":"7_CR29"},{"key":"7_CR30","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal Logic Can Be More Expressive. Information and Control 56. pages 71\u201399, 1983","journal-title":"Information and Control"},{"doi-asserted-by":"crossref","unstructured":"P. Zave and R. T. Yeh. Executable requirement specification for embedded system. Proc. 5th Int. Conf. on Software Engineering, San Diego, California, pages 295\u2013304, 1981.","key":"7_CR31","DOI":"10.21236\/ADA105459"},{"issue":"3","key":"7_CR32","first-page":"250","volume":"SE-8","author":"P. Zave","year":"1982","unstructured":"P. Zave An operational approach to requirements specifications. IEEE Trans. SE-8(3), pages 250\u2013269, 1982.","journal-title":"IEEE Trans"},{"key":"7_CR33","volume-title":"International Workshop on Comparing Systems Specification Techniques","author":"Y. Mokhtari","year":"1998","unstructured":"Y. Mokhtari The invoice system problem in TLA+ Proc. International Workshop on Comparing Systems Specification Techniques, University of Nantes, France March 1998."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48242-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T01:51:50Z","timestamp":1587779510000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48242-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664925","9783540482420"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-48242-3_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}