{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:07:57Z","timestamp":1776373677320,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540231677","type":"print"},{"value":"9783540302063","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30206-3_15","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:19:15Z","timestamp":1295345955000},"page":"199-214","source":"Crossref","is-referenced-by-count":39,"title":["Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol Using Calendar Automata"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Dutertre","sequence":"first","affiliation":[]},{"given":"Maria","family":"Sorea","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Bensalem, S., Ganesh, V., Lakhnech, Y., Mu\u00f1oz, C., Owre, S., Rue\u00df, H., Rushby, J., Rusu, V., Sa\u00efdi, H., Shankar, N., Singerman, E., Tiwari, A.: An overview of SAL. In: Fifth NASA Langley Formal Methods Workshop, NASA Langley Research Center, pp. 187\u2013196 (2000)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: Tool presentation: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/10722167_38","volume-title":"Computer Aided Verification","author":"J. Rushby","year":"2000","unstructured":"Rushby, J.: Verification diagrams revisited: Disjunctive invariants for easy verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 508\u2013520. Springer, Heidelberg (2000)"},{"key":"15_CR4","unstructured":"Steiner, W., Paulitsch, M.: The transition from asynchronous to synchronous system operation: An approach for distributed fault- tolerant systems. In: The 22nd International Conference on Distributed Computing Systems, ICDCS 2002 (2002)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal: Status and developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 456\u2013459. Springer, Heidelberg (1997)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: A modelchecking tool for real-time systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 546\u2013550. Springer, Heidelberg (1998)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-36384-X_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Wang","year":"2002","unstructured":"Wang, F.: Efficient verification of timed automata with BDD-like data-structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 189\u2013205. Springer, Heidelberg (2002)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 122\u2013125. Springer, Heidelberg (2003)"},{"key":"15_CR9","first-page":"166","volume-title":"Real-Time Systems Symposium (RTSS 2003)","author":"D. Kaynar","year":"2003","unstructured":"Kaynar, D., Lynch, N., Segala, R., Vaandrager, F.: Timed I\/O automata: A mathematical framework for modeling and analyzing real-time systems. In: Real-Time Systems Symposium (RTSS 2003), pp. 166\u2013177. IEEE Computer Society, Los Alamitos (2003)"},{"key":"15_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-06784-0","volume-title":"Duration Calculus: A Formal Approach to Real-Time Systems","author":"Z. Chaochen","year":"2004","unstructured":"Chaochen, Z., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J.U. Skakkeb\u00e6k","year":"1994","unstructured":"Skakkeb\u00e6k, J.U., Shankar, N.: Towards a duration calculus proof assistant in PVS. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol.\u00a0863, Springer, Heidelberg (1994)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Archer, M., Heitmeyer, C.: Mechanical verification of timed automata: A case study. Technical Report NRL\/MR\/5546-98-8180, Naval Research Laboratory, Washington, DC (1998)","DOI":"10.21236\/ADA359891"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"15_CR14","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on demand for satisfiability solvers. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing (2002)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 14\u201326. Springer, Heidelberg (2003)"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1006\/inco.1994.1060","volume":"112","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: Temporal proof methodologies for timed transition systems. Information and Computation\u00a0112, 273\u2013337 (1994)","journal-title":"Information and Computation"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0032002","volume-title":"Real-Time: Theory in Practice","author":"N. Lynch","year":"1992","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations for timing-based systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 397\u2013446. Springer, Heidelberg (1992)"},{"key":"15_CR19","unstructured":"Dutertre, B., Sorea, M.: Timed systems in SAL. Technical report, SRI-SDL-04-03, SRI International, Menlo Park, CA (2004)"},{"key":"15_CR20","unstructured":"Sorea, M.: Bounded model checking for timed automata. Electronic Notes in Theoretical Computer Science, vol. 68 (2002), http:\/\/www.elsevier.com\/locate\/entcs\/volume68.html"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Steiner, W., Rushby, J., Sorea, M., Pfeifer, H.: Model checking a fault-tolerant startup algorithm: From design exploration to exhaustive fault simulation. In: DSN 2004 (2004)","DOI":"10.1109\/DSN.2004.1311889"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"726","DOI":"10.1007\/3-540-57887-0_123","volume-title":"Theoretical Aspects of Computer Software","author":"Z. Manna","year":"1994","unstructured":"Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 726\u2013765. Springer, Heidelberg (1994)"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Yokogawa, T., Tsuchiya, T., Kikuno, T.: Automatic verification of fault tolerance using model checking. In: 2001 Pacific Rim International Symposium on Dependable Computing, Seoul, Korea (2001)","DOI":"10.1109\/PRDC.2001.992685"},{"key":"15_CR24","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1002\/stvr.258","volume":"12","author":"C. Bernardeschi","year":"2002","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S.: Model checking fault tolerant systems. Software Testing, Verification and Reliability\u00a012, 251\u2013275 (2002)","journal-title":"Software Testing, Verification and Reliability"},{"key":"15_CR25","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1109\/PRFTS.1997.640153","volume-title":"Pacific Rim International Symposium on Fault-Tolerant Systems (PRFTS 1997)","author":"H. L\u00f6nn","year":"1997","unstructured":"L\u00f6nn, H., Pettersson, P.: Formal verification of a TDMA protocol start-up mechanism. In: Pacific Rim International Symposium on Fault-Tolerant Systems (PRFTS 1997), pp. 235\u2013242. IEEE Computer Society, Los Alamitos (1997)"},{"key":"15_CR26","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. Int. Journal on Software Tools for Technology Transfer\u00a01, 134\u2013152 (1997)","journal-title":"Int. Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30206-3_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:48:35Z","timestamp":1605761315000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30206-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231677","9783540302063"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30206-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}