{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:46:46Z","timestamp":1725454006002},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540638889"},{"type":"electronic","value":"9783540696612"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0000471","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T06:30:36Z","timestamp":1128493836000},"page":"185-198","source":"Crossref","is-referenced-by-count":3,"title":["Software design, specification, and verification: Lessons learned from the Rether case study"],"prefix":"10.1007","author":[{"given":"Xiaoqun","family":"Du","sequence":"first","affiliation":[]},{"given":"Kevin T.","family":"McDonnell","sequence":"additional","affiliation":[]},{"given":"Evangelos","family":"Nanos","sequence":"additional","affiliation":[]},{"given":"Y. S.","family":"Ramakrishna","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,9,7]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"R. Alur and D. Dill. The theory of timed automata. TCS, 126(2), 1994.","key":"13_CR1","DOI":"10.1016\/0304-3975(94)90010-8"},{"doi-asserted-by":"crossref","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 Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52\u201371. Springer-Verlag, 1981.","key":"13_CR2","DOI":"10.1007\/BFb0025774"},{"doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.","key":"13_CR3","DOI":"10.1145\/5397.5399"},{"key":"13_CR4","series-title":"volume 1102 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/3-540-61474-5_88","volume-title":"Computer Aided Verification (CAV '96)","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland, P. M. Lewis, S. A. Smolka, and O. Sokolsky. The Concurrency Factory: A development environment for concurrent systems. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 398\u2013401, New Brunswick, New Jersey, July 1996. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"T. Chiueh and C. Venkatramani. The design, implementation and evaluation of a software-based real-time ethernet protocol. In Proceedings of ACM SIG-COMM '95, pages 27\u201337, 1995.","key":"13_CR5","DOI":"10.1145\/217382.217404"},{"doi-asserted-by":"crossref","unstructured":"E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4), December 1996.","key":"13_CR6","DOI":"10.1145\/242223.242257"},{"key":"13_CR7","volume-title":"Proceedings of the 9th International Conference on Computer-Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In Proceedings of the 9th International Conference on Computer-Aided Verification, Haifa, Israel, July 1997. Springer-Verlag."},{"key":"13_CR8","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u039c-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"13_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1995.1024","volume":"117","author":"K. L. McMillan","year":"1995","unstructured":"K. L. McMillan and R. Kurshan. A structural induction theorem for processes. Information and Computation, 117:1\u201311, 1995.","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"A. K. Mok. Toward mechanization of real-time system design. In A. van Tilborg and G. Koob, editors, Foundations of Real-Time Computing: Formal Specifications and Methods, pages 1\u201338. Kluwer Academic Publishers, 1991.","key":"13_CR10","DOI":"10.1007\/978-1-4615-4016-8_1"},{"issue":"2","key":"13_CR11","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/2.485847","volume":"29","author":"D. L. Parnas","year":"1996","unstructured":"D. L. Parnas. Why software jewels are rare. IEEE Computer, 29(2):57\u201361, February 1996.","journal-title":"IEEE Computer"},{"key":"13_CR12","series-title":"volume 137 of Lecture Notes in Computer Science","volume-title":"Proceedings of the International Symposium in 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 the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"Y. S. Ramakrishna and S. A. Smolka. Partial-order reduction in the weak modal mu-calculus. In Proceedings of the Eighth International Conference on Concurrency Theory (CONCUR '97). Springer-Verlag, July 1997.","key":"13_CR13","DOI":"10.1007\/3-540-63141-0_2"},{"key":"13_CR14","series-title":"volume 939 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer Aided Verification (CAV '95)","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In P. Wolper, editor, Computer Aided Verification (CAV '95), volume 939 of Lecture Notes in Computer Science, pages 84\u201397, Li\u00e9ge, Belgium, July 1995. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"O. Sokolsky and S. A. Smolka. Local model checking for real-time systems. In Proceedings of the 7th International Conference on Computer-Aided Verification. American Mathematical Society, 1995.","key":"13_CR15","DOI":"10.1007\/3-540-60045-0_52"},{"doi-asserted-by":"crossref","unstructured":"B. Thomsen, L. Leth, and T.-M. Kuo. A Facile tutorial. In Proceedings of the Seventh International Conference on Concurrency Theory (CONCUR '96), Vol. 1119 of Lecture Notes in Computer Science, pages 278\u2013298. Springer-Verlag, 1996.","key":"13_CR16","DOI":"10.1007\/3-540-61604-7_61"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000471","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T22:22:03Z","timestamp":1586470923000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000471"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540638889","9783540696612"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0000471","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}