{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T22:49:31Z","timestamp":1729637371808,"version":"3.28.0"},"reference-count":14,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/ipdps.2001.925137","type":"proceedings-article","created":{"date-parts":[[2005,8,29]],"date-time":"2005-08-29T12:47:11Z","timestamp":1125319631000},"page":"1526-1533","source":"Crossref","is-referenced-by-count":2,"title":["Specifying and verifying a railroad crossing with cafeOBJ"],"prefix":"10.1109","author":[{"given":"K.","family":"Ogata","sequence":"first","affiliation":[]},{"given":"K.","family":"Futatsugi","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"journal-title":"Distributed Algorithms","year":"1996","author":"lynch","key":"ref10"},{"journal-title":"The Temporal Logic of Reactive and Concurrent Systems Specification","year":"1991","author":"manna","key":"ref11"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46674-6_24"},{"key":"ref14","first-page":"159","article-title":"Specification and verification of some classical mutual exclusion algorithms with cafeobj","author":"ogata","year":"1999","journal-title":"OBJ\/CafeOBJ\/Maude at Formal Methods '99"},{"journal-title":"Parallel Program Design A Foundation","year":"1988","author":"chandy","key":"ref4"},{"journal-title":"CafeOBJ web page","year":"0","key":"ref3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00275-3"},{"key":"ref5","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume":"6","author":"diaconescu","year":"1998","journal-title":"CafeOBJ report AMAST Series in Computing"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050177"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/BFb0020933","author":"kesten","year":"1996","journal-title":"Verifying clocked transition systems in Hybrid Systems III Verification and Control"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186058"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"}],"event":{"name":"IEEE International Symposium on Parallel and Distributed Processing","acronym":"IPDPS-01","location":"San Francisco, CA, USA"},"container-title":["Proceedings 15th International Parallel and Distributed Processing Symposium. IPDPS 2001"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/7373\/20001\/00925137.pdf?arnumber=925137","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T07:13:58Z","timestamp":1586416438000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/925137\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":14,"URL":"https:\/\/doi.org\/10.1109\/ipdps.2001.925137","relation":{},"subject":[]}}