{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:02Z","timestamp":1725484082384},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540411864"},{"type":"electronic","value":"9783540408918"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40891-6_5","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T20:01:38Z","timestamp":1180209698000},"page":"53-63","source":"Crossref","is-referenced-by-count":2,"title":["Validation of Control System Specifications with Abstract Plant Models"],"prefix":"10.1007","author":[{"given":"Wenhui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and E. A. Emerson and A. P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages: 117\u2013126, January 1983.","DOI":"10.1145\/567067.567080"},{"key":"5_CR2","series-title":"OECD Halden Reactor Project Report","volume-title":"Verification and Validation of Human Factors Issues in Control Room Design and Upgrades","author":"S. Collier","year":"1999","unstructured":"S. Collier and M. Green. Verification and Validation of Human Factors Issues in Control Room Design and Upgrades. OECD Halden Reactor Project Report: HWR-598, Institute for Energy Technology, Norway. 1999."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and Model Logic. Handbook of theoretical computer science, Volume B: Formal Models and Semantics (ed. Jan van Leeuwen). Elsevier. 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"5_CR4","unstructured":"P. Godefroid and G. J. Holzmann. On the Verification of Temporal Properties. Protocol Specification, Testing and Verification, XIII (C-16). A. Dantine, G. Leduc and P. Walper (Eds). 1993."},{"key":"5_CR5","series-title":"OECD Halden Reactor Project Report","volume-title":"OECD Halden Reactor Project: COPMA II On-Line Functional Specifications","author":"F. Handelsby","year":"1992","unstructured":"F. Handelsby, E. Ness and J. Teigen. OECD Halden Reactor Project: COPMA II On-Line Functional Specifications. OECD Halden Reactor Project Report: HWR-319, Institute for Energy Technology, Norway. 1992."},{"issue":"5","key":"5_CR6","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":"5_CR7","doi-asserted-by":"crossref","unstructured":"M. H. Lipner and S. P. Kerch. Operational Benefits of an Advanced Computerised Procedure System. 1994 IEEE Conference Record: Nuclear Science Symposium andMed ical Imaging Conference: 1068\u20131072. 1995.","DOI":"10.1109\/NSSMIC.1994.474658"},{"issue":"4","key":"5_CR8","first-page":"504","volume":"31","author":"L. Reynes","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":"5_CR9","unstructured":"H. Roth-Seefrid, J. Erdmann, L. Simon and M. Dull. SiROG: A Computer-based Manual for Situation Related Operator Guidance. Presentation at the Enlarged Halden Programme Group Meeting. Bolkesj\u00f8, Norway. October 1994."},{"key":"5_CR10","series-title":"OECD Halden Reactor Project Report","volume-title":"Algebraic Specification andT heorem Proving used in Formal Verification of Discrete Event Control Systems","author":"T. Sivertsen","year":"1989","unstructured":"T. Sivertsen and H. Valisuo. Algebraic Specification andT heorem Proving used in Formal Verification of Discrete Event Control Systems. OECD Halden Reactor Project Report: HWR-260, Institute for Energy Technology, Norway. 1989."},{"key":"5_CR11","volume-title":"Logical Validation of Safety and Control System Specifications Against Plant Models","author":"J. R. Taylor","year":"1981","unstructured":"J. R. Taylor. Logical Validation of Safety and Control System Specifications Against Plant Models. Ris\u00f8 National Laboratory, Roskilde, Danmark. 1981."},{"key":"5_CR12","series-title":"OECD Halden Reactor Project Report","volume-title":"COPMA-III \u2014 Software Design andI mplementation Issues","author":"J. Teigen","year":"1998","unstructured":"J. Teigen and J. E. Hulsund. COPMA-III \u2014 Software Design andI mplementation Issues. OECD Halden Reactor Project Report: HWR-509, Institute for Energy Technology, Norway. 1998."},{"key":"5_CR13","first-page":"322","volume":"1","author":"M. Y. Vardi","year":"1986","unstructured":"M. Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. IEEE Symposium on Logic in Computer Science 1: 322\u2013331, 1986.","journal-title":"IEEE Symposium on Logic in Computer Science"},{"key":"5_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-48234-2_16","volume-title":"Model Checking Operator Procedures","author":"W. Zhang","year":"1999","unstructured":"W. Zhang. Model Checking Operator Procedures. Proceedings of the 6th International SPIN Workshop on Practical Aspects of Model Checking (Lecture Notes in Computer Science 1680: 200\u2013215). Toulouse, France. 1999."}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40891-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:03:25Z","timestamp":1556435005000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40891-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540411864","9783540408918"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-40891-6_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}