{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:40:23Z","timestamp":1737355223519,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_36","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"535-549","source":"Crossref","is-referenced-by-count":7,"title":["A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors"],"prefix":"10.1007","author":[{"given":"S.","family":"Gnesi","sequence":"first","affiliation":[]},{"given":"D.","family":"Latella","sequence":"additional","affiliation":[]},{"given":"G.","family":"Lenzini","sequence":"additional","affiliation":[]},{"given":"C.","family":"Abbaneo","sequence":"additional","affiliation":[]},{"given":"A.","family":"Amendola","sequence":"additional","affiliation":[]},{"given":"P.","family":"Marmo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"issue":"12","key":"36_CR1","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"2","author":"C. Bernardeschi","year":"1998","unstructured":"C. Bernardeschi, A. Fantechi, S. Gnesi, S. Larosa, G. Mongardi, and D. Romano. A Formal Verification Environment for Railway Signaling System Design. Formal Methods in System Design, 2(12):139\u2013161, 1998. 536","journal-title":"Formal Methods in System Design"},{"key":"36_CR2","unstructured":"A. Bor\u00e4lv. A Fully Automated Approach for Proving Safety Properties in Interlocking Software Using Automatic Theorem-Proving. In Proceedings of the 2nd International ERCIM Workshop on Formal Methods Industrial Critical Systems, 1997. 536"},{"issue":"4","key":"36_CR3","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/s001650050022","volume":"10","author":"A. Cimatti","year":"1998","unstructured":"A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, and P. Traverso. Formal Verification of a Railway Interlocking System using Model Checking. Formal Aspect of Computing, 10(4):361\u2013380, 1998. 536","journal-title":"Formal Aspect of Computing"},{"key":"36_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specification. ACM Transaction on Programming Languages and Systems, 8:244\u2013263, 1986. 536","journal-title":"ACM Transaction on Programming Languages and Systems"},{"issue":"6","key":"36_CR5","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/390016.808417","volume":"10","author":"E. W. Dijkstra","year":"1975","unstructured":"E. W. Dijkstra. Guarded Commands, Non-Determinacy and a Calculus for The Derivation of Programs. ACM SIGPLAN Notices, 10(6):2\u201314, June 1975. 538","journal-title":"ACM SIGPLAN Notices"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Cindy Eisner. Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Keersenboogerd and Heerhugowaard. In Proceedings of CHARME\u2019 99, 1999. 536","DOI":"10.1007\/3-540-48153-2_9"},{"key":"36_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings of the Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In D. Kozen, editor, Proceedings of the Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52\u201371, Yorktown Heights, New York, 1981. Springer-Verlag. 536"},{"key":"36_CR8","unstructured":"W. J. Fokkink. Safey Criteria for Hoorn-Keersenboogerd Railway Station. Technical Report Preprint Series 135, Utrecht, 1995. 536"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"J. F. Groote, S. F.M. van Vlijemn, and J. W. C. Koorn. The Safety Guaranteeing System at Station Hoorn-Kersenboogerd in Propositional Logic. In Proceedings of 10th Annual Conference on Computer Assurance (COMPASS\u201995), pages 57\u201368, 1995. 536","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"36_CR10","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prantice-Hall International, 1991. 538"},{"key":"36_CR11","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991. 536, 538"},{"issue":"23","key":"36_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"5","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The Model Checker SPIN. IEEE Transaction on Software Engineering, 5(23):279\u2013295, 1997. 536, 538","journal-title":"IEEE Transaction on Software Engineering"},{"key":"36_CR13","unstructured":"IEC 61508 IEC. Functional safety of electrical\/electronic\/programmable electronic safety-related systems. 536"},{"issue":"3","key":"36_CR14","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L. Lamport","year":"1982","unstructured":"L. Lamport, R. Shostak, and M. Pease. The Byzantine Generals Problem. ACM Transaction on Programming Languages and Systems, 4(3):382\u2013401, 1982. 536, 542","journal-title":"ACM Transaction on Programming Languages and Systems"},{"issue":"7","key":"36_CR15","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/52.493020","volume":"13","author":"P. G. Larsen","year":"1996","unstructured":"P. G. Larsen, J. Fitzgerald, and T. Brookers. Applying Formal Specification in Industry. IEEE Software, 13(7):48\u201356, 1996. 536","journal-title":"IEEE Software"},{"key":"36_CR16","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s002870050102","volume":"21","author":"P. Liggersmeyer","year":"1998","unstructured":"P. Liggersmeyer, M. Rothfelder, M. Rettelbach, and T. Ackermann. Qualit\u00e4tssincherung Software-basierter Technischer Systeme-Problembereiche und L\u00f6sungs\u00e4nsatze. Informatik Spektrum, 21:249\u2013258, 1998. in German. 535","journal-title":"Informatik Spektrum"},{"key":"36_CR17","doi-asserted-by":"crossref","unstructured":"G. Mongardi. Dependable Computing for Railway Control System, chapter 3. Springer-Verlag, 1993. 536","DOI":"10.1007\/978-3-7091-4009-3_11"},{"key":"36_CR18","first-page":"147","volume":"29","author":"M. J. Morely","year":"1997","unstructured":"M. J. Morely. Safety-Level Communication in Railway Interlockings. Science of Communication, 29:147\u2013170, 1997. 536","journal-title":"Science of Communication"},{"key":"36_CR19","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-77), pages 46\u201357, Providence, Rhode Island, 1977. IEEE, IEEE Computer Society Press. 538","DOI":"10.1109\/SFCS.1977.32"},{"key":"36_CR20","unstructured":"pr EN 50128 CENELEC. Railways Applications: Software for Railway Control and Protection Systems. 536"},{"key":"36_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of 5th International Symposium on Programming","author":"J. P. Queille","year":"1982","unstructured":"J. P. Queille and J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. In Proceedings of 5th International Symposium on Programming, Lecture Notes in Computer Science, Vol. 137, pages 337\u2013371. SV, Berlin\/New York, 1982."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:00:08Z","timestamp":1737352808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}