{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:09:50Z","timestamp":1742396990567,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664994"},{"type":"electronic","value":"9783540482345"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48234-2_16","type":"book-chapter","created":{"date-parts":[[2007,10,30]],"date-time":"2007-10-30T03:58:10Z","timestamp":1193716690000},"page":"200-215","source":"Crossref","is-referenced-by-count":7,"title":["Model Checking Operator Procedures"],"prefix":"10.1007","author":[{"given":"Wenhui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,8,27]]},"reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"A. M","year":"1995","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3):507\u2013534. May 1995.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR2","unstructured":"J. R. Burch, E. M. Clarke and D. E. Long. Symbolic Model Checking with Partitioned Transition Relations. International Conference on Very Large Scale Integration, pp. 49\u201358. North-Holland, August 1991."},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D. E. Long. Model Checking and Modular Verification. ACM Transactions on Programming Languages and Systems 16(3):843\u2013871. May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR4","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1177\/154193129403800402","volume":"1","author":"D.G. Hoecker","year":"1994","unstructured":"D. G. Hoecker, K. M. Corker, E. M. Roth, M. H. Lipner and M. S. Bunzo. Man-Machine Design and Analysis System (MIDAS) Applied to a Computer-Based Procedure-Aiding System. Proceedings of the Human Factors and Ergonomics Society 38th Annual Meeting 1: 195\u2013199. 1994.","journal-title":"Proceedings of the Human Factors and Ergonomics Society 38th Annual Meeting"},{"issue":"5","key":"16_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The Model Checker Spin. IEEE Transaction on Software Engineering 23(5): 279\u2013295. 1997.","journal-title":"IEEE Transaction on Software Engineering"},{"key":"16_CR6","unstructured":"J. G. Kemeny. Report of the President\u2019s Commission on the Accident at Three Mile Island. U.S. Government Accounting Office. 1979."},{"key":"16_CR7","unstructured":"N. G. Leveson.Software System Safety and Computers. Addison-Wesley Publishing Company. 1995."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"M. H. Lipner and S. P. Kerch. Operational Bene-ts of an Advanced Computerised Procedure System. 1994 IEEE Conference Record: Nuclear Science Symposium and Medical Imaging Conference:(1068\u20131072). 1995.","DOI":"10.1109\/NSSMIC.1994.474658"},{"issue":"4","key":"16_CR9","first-page":"504","volume":"31","author":"R. L","year":"1990","unstructured":"L. Reynes and G. Beltranda. A Computerised Control Room to Improve Nuclear Power Plant Operation and Safety. Nuclear Safety 31(4):504\u2013511. 1990.","journal-title":"Nuclear Safety"},{"key":"16_CR10","volume-title":"OECD Halden Reactor Project Report","author":"S. T","year":"1989","unstructured":"T. Sivertsen and H. Valisuo. Algebraic Specification and Theorem Proving used in Formal Verification of Discrete Event Control Systems. OECD Halden Reactor Project Report: HWR-260, Institute for Energy Technology, Norway. 1989."},{"key":"16_CR11","volume-title":"OECD Halden Reactor Project Report","author":"J. Teigen","year":"1998","unstructured":"J. Teigen and J. E. Hulsund. COPMA-III-Software Design and Implementation Issues. OECD Halden Reactor Project Report: HWR-509, Institute for Energy Technology, Norway. 1998."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"H. J. Touati, H. Savoj, B. Lin, R. K. Brayton and A. Sangiovanni-Vincentelli. Implicit State Enumeration of Finite State Machines Using BDDs. IEEE International Conference on Computer-Aided Design, pp. 130\u2013133. IEEE Computer Society Press, November 1990.","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"16_CR13","volume-title":"OECD Halden Reactor Project Report","author":"Y. K","year":"1992","unstructured":"K. Ylikoski and G. Dahll. Verification of Procedures. OECD Halden Reactor Project Report: HWR-318, Institute for Energy Technology, Norway. 1992."}],"container-title":["Lecture Notes in Computer Science","Theoretical and Practical Aspects of SPIN Model Checking"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48234-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T00:40:10Z","timestamp":1737506410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48234-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664994","9783540482345"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48234-2_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}