{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:07:40Z","timestamp":1725516460893},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642317583"},{"type":"electronic","value":"9783642317590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31759-0_20","type":"book-chapter","created":{"date-parts":[[2012,7,19]],"date-time":"2012-07-19T00:59:50Z","timestamp":1342659590000},"page":"255-260","source":"Crossref","is-referenced-by-count":2,"title":["S2N: Model Transformation from SPIN to NuSMV"],"prefix":"10.1007","author":[{"given":"Yong","family":"Jiang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-45510-8_1","volume-title":"Modeling and Verification of Parallel Processes","author":"S. Merz","year":"2001","unstructured":"Merz, S.: Model Checking: A Tutorial Overview. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, pp. 3\u201338. Springer, Heidelberg (2001)"},{"key":"20_CR2","unstructured":"Holzmann, G.J.: The Spin model checker: Primer and reference manual. Addison-Wesley (2004)"},{"key":"20_CR3","unstructured":"NuSMV tutorial, \n                    \n                      http:\/\/nusmv.fbk.eu\/NuSMV\/tutorial\/index.html"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/3-540-45139-0_11","volume-title":"Model Checking Software","author":"M. Baldamus","year":"2001","unstructured":"Baldamus, M., Schr\u00f6der-Babo, J.: p2b: A Translation Utility for Linking Promela and Symbolic Model Checking (Tool Paper). In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 183\u2013191. Springer, Heidelberg (2001)"},{"issue":"3","key":"20_CR5","first-page":"387","volume":"3","author":"L.M. Ruane","year":"1990","unstructured":"Ruane, L.M.: Process synchronization in the UTS kernel. Computing systems\u00a03(3), 387\u2013421 (1990)","journal-title":"Computing systems"},{"issue":"6","key":"20_CR6","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1109\/32.926177","volume":"27","author":"K.-S. Bang","year":"2001","unstructured":"Bang, K.-S., Choi, J.-Y., Yoo, C.: Comments on \u201cThe model checker Spin\u201d. IEEE Transactions on Software Engineering\u00a027(6), 573\u2013576 (2001)","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31759-0_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:47:30Z","timestamp":1620128850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31759-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642317583","9783642317590"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31759-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}