{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:54Z","timestamp":1725664854335},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635338"},{"type":"electronic","value":"9783540695936"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63533-5_20","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:29:03Z","timestamp":1330298943000},"page":"378-397","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["TLA + PROMELA: Conjecture, check, proof"],"prefix":"10.1007","author":[{"given":"J. -Ch.","family":"Gr\u00e9goire","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Stephan Merz. On TLA as a logic. In Manfred Broy, editor, Deductive Program Design, pages 235\u2013271. NATO ASI Series, Springer-Verlag, 1995.","DOI":"10.1007\/978-3-642-61455-2_14"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"20_CR3","unstructured":"J. Hajek. Automatically verified data transfer protocols. In 4th ICCC pages 749\u2013756, 1978."},{"key":"20_CR4","series-title":"number 1051 in Lecture Notes in Computer Science","first-page":"662","volume-title":"Formal Methods Europe FME '96","author":"K. Havelund","year":"1996","unstructured":"Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, number 1051 in Lecture Notes in Computer Science, pages 662\u2013681, Oxford, UK, March 1996. Springer-Verlag."},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"P. Herrmann and H. Krumm. Re-usable verification elements for high-speed transfer protocol configu ration. In Protocol Specification, Testing and Verification XV, pages 171\u2013186. Chapman & Hall, 1995.","DOI":"10.1007\/978-0-387-34892-6_11"},{"key":"20_CR6","unstructured":"Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Gerard J. Holzmann and Doron Peled. An improvement in formal verification. In Dieter Hogrefe and Stefan Leue, editors, 7th Int. Conf. on Formal Description Techniques. Chapman and Hall, 1994.","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"20_CR8","unstructured":"Peter Ladkin. Formal but lively buffers in TLA+. Technical report, Universit\u00e4t von Bielefeld, 1996. from http:\/\/www.rvs.uni-bielefeld.de\/."},{"issue":"3","key":"20_CR9","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872\u2013923, 1994.","journal-title":"ACM TOPLAS"},{"key":"20_CR10","unstructured":"Leslie Lamport. TLA+. Technical report, DEC-SRC, 1995. from http:\/\/www.research.digital.com\/SRC\/personal\/Leslie-Lamport\/tla\/papers.html."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Zoar Manna and Amir Pnueli. A Temporal Proof Methodology for Reactive Systems. In Program Design Calculi, NATO ASI Series, Series F. Springer Verlag, 1993.","DOI":"10.21236\/ADA262848"},{"key":"20_CR12","unstructured":"Natarajan and G.J. Holzmann. Towards a formal semantics of PROMELA. In Proceedings of the 2nd SPIN Workshop, 1996."},{"issue":"2","key":"20_CR13","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification of fault-tolerant architectures: Prolegmena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","FME '97: Industrial Applications and Strengthened Foundations of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63533-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T11:50:09Z","timestamp":1640951409000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_20"}},"subtitle":["Engineering new protocols using methods and formal notations"],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}