{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:50Z","timestamp":1725664850532},"publisher-location":"Berlin, Heidelberg","reference-count":22,"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_31","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:29:10Z","timestamp":1330280950000},"page":"589-604","source":"Crossref","is-referenced-by-count":10,"title":["Verification of reactive systems using DisCo and PVS"],"prefix":"10.1007","author":[{"given":"Pertti","family":"Kellom\u00e4ki","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"31_CR1","unstructured":"The DisCo project home page. http:\/\/www.cs.tut.fi\/laitos\/DisCo\/."},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Sten Agerholm. Translating specifications in VDM-SL to PVS. In J. von Wright, T. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 1\u201316. Springer-Verlag, 1996.","DOI":"10.1007\/BFb0105393"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"F. Andersen, K. D. Petersen, and J. S. Petterson. Program verification using HOLUNITY. In J. J. Joyce and C.-J.H Seger, editors, International Workshop on Higher Order Logic and its Applications, volume 780 of Lecture Notes in Computer Science, pages 1\u201316, 1994.","DOI":"10.1007\/3-540-57826-9_121"},{"issue":"4","key":"31_CR4","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1145\/48022.48023","volume":"10","author":"R. J. R. Back","year":"1988","unstructured":"R. J. R. Back and R. Kurki-Suonio. Distributed cooperation with action systems. ACM Transactions on Programming Languages and Systems, 10(4):513\u2013554, October 1988.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with a centralized control. Distributed Computing, (3):73\u201387, 1989.","DOI":"10.1007\/BF01558665"},{"issue":"5","key":"31_CR6","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K. A. Bartlett","year":"1969","unstructured":"K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260\u2013261, May 1969.","journal-title":"Communications of the ACM"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"issue":"5","key":"31_CR8","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269\u2013276, December 1991.","journal-title":"Information Processing Letters"},{"key":"31_CR9","series-title":"Technical Report RR 2475","volume-title":"Formal Verification of Concurrent Programs: How to specify UNITY using the Larch Prover","author":"B. Chetali","year":"1995","unstructured":"B. Chetali. Formal Verification of Concurrent Programs: How to specify UNITY using the Larch Prover. Technical Report RR 2475, INRIA-Lorraine, Nancy, France, January 1995."},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Ching-Tsun Chou. Mechanical verification of distributed algorithms in higher-order logic. The Computer Journal, 38(1), 1995.","DOI":"10.1093\/comjnl\/38.2.152"},{"key":"31_CR11","unstructured":"Urban Engberg, Peter Gr\u00f8nning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In G. v. Bochmann and D. K. Probst, editors, Computer Aided Verification\u2013Fourth International Workshop. CAV'92. Montreal, Canada. June 29\u2013July 1, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, 1992."},{"issue":"3","key":"31_CR12","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231\u2013274, June 1987.","journal-title":"Science of Computer Programming"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. Lecture Notes in Computer Science, 1051, 1996.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Barbara Heyd and Pierre Cr\u00e9gut. A modular coding of UNITY in COQ. In J. von Wright, T. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 251\u2013266, 1996.","DOI":"10.1007\/BFb0105409"},{"key":"31_CR15","unstructured":"Haxmu-Matti Jarvinen. The Design of a Specification Language for Reactive Systems. PhD thesis, Tampere University of Technology, 1992."},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"S. Kalvala. A formulation of TLA in Isabelle. Lecture Notes in Computer Science, 971, 1995.","DOI":"10.1007\/3-540-60275-5_67"},{"key":"31_CR17","unstructured":"Reino Kurki-Suonio, Hannu-Matti J\u00e4rvinen, Markku Sakkinen, and Kari Syst\u00e4. Object-oriented specification of reactive systems. In Proceedings of the 12th International Conference on Software Engineering, pages 63\u201371. IEEE Computer Society Press, 1990."},{"issue":"3","key":"31_CR18","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 Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Thomas L\u00e5ngbacka. A HOL formalization of the temporal logic of actions. volume 859 of Lecture Notes in Computer Science. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58450-1_52"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752. Springer Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/3-540-58468-4_189","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J. U. Skakkebaek","year":"1994","unstructured":"Jens U. Skakkebaek and N. Shankar. Towards a Duration Calculus proof assistant in PVS. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 660\u2013679, L\u00fcbeck, Germany, September 1994. Springer-Verlag."},{"key":"31_CR22","unstructured":"J. von Wright and T. L\u00e5ngbacka. Using a theorem prover for reasoning about concurrent algorithms. In G. v. Bochmann and D. K. Probst, editors, Computer Aided Verification \u2014 Fourth International Workshop. CAV'92. Montreal, Canada. June 29\u2013July 1, volume 663 of Lecture Notes in Computer Science. Springer Verlag, 1992."}],"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_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:18:52Z","timestamp":1605629932000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}