{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T18:40:29Z","timestamp":1771008029835,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540291053","type":"print"},{"value":"9783540320302","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_14","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"162-175","source":"Crossref","is-referenced-by-count":56,"title":["Real-Time Model Checking Is Really Simple"],"prefix":"10.1007","author":[{"given":"Leslie","family":"Lamport","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"14_CR1","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M. Abadi","year":"1994","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems\u00a016(5), 1543\u20131571 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"5","key":"14_CR2","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-30206-3_15","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"B. Dutertre","year":"2004","unstructured":"Dutertre, B., Sorea, M.: Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 199\u2013214. Springer, Heidelberg (2004)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"644","DOI":"10.1007\/3-540-56610-4_95","volume-title":"TAPSOFT \u201993: Theory and Practice of Software Development","author":"S. Graf","year":"1993","unstructured":"Graf, S., Loiseaux, C.: Property preserving abstractions under parallel composition. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol.\u00a0668, pp. 644\u2013657. Springer, Heidelberg (1993)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/BFb0014712","volume-title":"Hybrid and Real-Time Systems","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Kupferman, O.: From quantity to quality. In: Maler, O. (ed.) HART 1997. LNCS, vol.\u00a01201, pp. 48\u201362. Springer, Heidelberg (1997)"},{"key":"14_CR6","volume-title":"The Spin Model Checker","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)"},{"issue":"1\u20132","key":"14_CR7","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/S0304-3975(98)00129-7","volume":"206","author":"L. Lamport","year":"1998","unstructured":"Lamport, L.: Proving possibility properties. Theoretical Computer Science\u00a0206(1\u20132), 341\u2013352 (1998)","journal-title":"Theoretical Computer Science"},{"key":"14_CR8","volume-title":"Specifying Systems","author":"L. Lamport","year":"2003","unstructured":"Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2003); A link to an electronic copy can be found at, \n                    \n                      http:\/\/lamport.org"},{"key":"14_CR9","unstructured":"Lamport, L.: Real time is really simple. Technical Report MSR-TR-2005-30, Microsoft Research (March 2005)"},{"issue":"1\/2","key":"14_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal of Software Tools for Technology Transfer\u00a01(1\/2), 134\u2013152 (1997)","journal-title":"International Journal of Software Tools for Technology Transfer"},{"key":"14_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)"},{"key":"14_CR12","series-title":"SIGCOMM","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/319056.319004","volume-title":"Proceedings of the Ninth Symposium on Data Communications","author":"R. Perlman","year":"1985","unstructured":"Perlman, R.: An algorithm for distributed computation of a spanningtree in an extended LAN. In: Proceedings of the Ninth Symposium on Data Communications. SIGCOMM, pp. 44\u201353. ACM Press, New York (1985)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"618","DOI":"10.1007\/BFb0032010","volume-title":"Real-Time: Theory in Practice","author":"F.B. Schneider","year":"1992","unstructured":"Schneider, F.B., Bloom, B., Marzullo, K.: Putting time into proof outlines. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 618\u2013639. Springer, Heidelberg (1992)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:13:09Z","timestamp":1619507589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11560548_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}