{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:13:19Z","timestamp":1767237199386},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,5,24]],"date-time":"2011-05-24T00:00:00Z","timestamp":1306195200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s11334-011-0152-5","type":"journal-article","created":{"date-parts":[[2011,5,23]],"date-time":"2011-05-23T08:35:16Z","timestamp":1306139716000},"page":"119-130","source":"Crossref","is-referenced-by-count":5,"title":["Using integer clocks to verify clock-synchronization protocols"],"prefix":"10.1007","volume":"7","author":[{"given":"Xiaowan","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anu","family":"Singh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,5,24]]},"reference":[{"key":"152_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Dill DL (1994) The theory of timed automata. TCS 126(2)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"152_CR2","doi-asserted-by":"crossref","unstructured":"Dutertre B, Sorea M (2004) Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In: FORMATS\/FTRTFT, pp 199\u2013214","DOI":"10.1007\/978-3-540-30206-3_15"},{"key":"152_CR3","doi-asserted-by":"crossref","unstructured":"Ganeriwal S, Kumar R, Srivastava MB (2003) Timing-sync protocol for sensor networks. In: Proceedings of the 1st international conference on embedded networked sensor systems (SenSys), ACM, pp 138\u2013149","DOI":"10.1145\/958491.958508"},{"key":"152_CR4","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1007\/978-3-642-05089-3_33","volume-title":"FM 2009: formal methods. Lecture Notes in Computer Science. vol 5850","author":"F Heidarian","year":"2009","unstructured":"Heidarian F, Schmaltz J, Vaandrager FW (2009) Analysis of a clock synchronization protocol for wireless sensor networks. In: Cavalcanti A, Dams D (eds) FM 2009: formal methods. Lecture Notes in Computer Science, vol 5850. Springer, Berlin, pp 516\u2013531"},{"key":"152_CR5","doi-asserted-by":"crossref","unstructured":"Henderson W, Tron S (2006) Verification of the minimum cost forwarding protocol for wireless sensor networks. In: IEEE conference on emerging technologies and factory automation, IEEE Computer Society, pp 516\u2013531","DOI":"10.1109\/ETFA.2006.355457"},{"key":"152_CR6","doi-asserted-by":"crossref","unstructured":"Huang X, Seyster J, Callanan S, Dixit K, Grosu R, Smolka SA, Stoller SD, Zadok E (2011) Software monitoring with controllable overhead. Int J Softw Tools Technol Transf (accepted for publication)","DOI":"10.1007\/s10009-010-0184-4"},{"key":"152_CR7","unstructured":"Huang X, Singh A, Smolka SA (2010) Using integer clocks to verify the timing-sync sensor network protocol. In: Proceedings of NFM 2010, second NASA formal methods symposium. NASA Conference Publication, April 2010"},{"key":"152_CR8","unstructured":"Kusy B, Abdelwahed S (2006) FTSP protocol verification using SPIN. Technical Report ISIS-06-704, Institute for Software Integrated Systems, May 2006"},{"issue":"1\u20132","key":"152_CR9","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf (STTT) 1(1\u20132): 134\u2013152","journal-title":"Int J Softw Tools Technol Transf (STTT)"},{"key":"152_CR10","doi-asserted-by":"crossref","unstructured":"Lenzen C, Locher T, Wattenhofer R (2009) Tight bounds for clock synchronization. In: PODC \u201909: Proceedings of the 28th ACM symposium on principles of distributed computing, ACM, pp 46\u201355","DOI":"10.1145\/1582716.1582730"},{"key":"152_CR11","doi-asserted-by":"crossref","unstructured":"Mar\u00f3ti M, Kusy B, Simon G, L\u00e9deczi A (2004) The flooding time synchronization protocol. In: Proceedings of the 2nd international conference on embedded networked sensor systems (SenSys), ACM, pp 39\u201349","DOI":"10.1145\/1031495.1031501"},{"key":"152_CR12","first-page":"748","volume-title":"11th International conference on automated deduction (CADE) Lecture Notes in Artificial Intelligence, vol 607, Saratoga, NY, June 1992.","author":"S Owre","year":"1992","unstructured":"Owre S, Rushby JM, Shankar N (1992) PVS: A prototype verification system. In: Kapur D (eds) 11th International conference on automated deduction (CADE) Lecture Notes in Artificial Intelligence, vol 607, Saratoga, NY, June 1992. Springer, Berlin, pp 748\u2013752"},{"key":"152_CR13","doi-asserted-by":"crossref","unstructured":"Pike L (2007) Modeling time-triggered protocols and verifying their real-time schedules. In: Proceedings of formal methods in computer aided design (FMCAD\u201907), IEEE, pp 231\u2013238","DOI":"10.1109\/FAMCAD.2007.10"},{"key":"152_CR14","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1109\/32.815324","volume":"25","author":"J Rushby","year":"1999","unstructured":"Rushby J (1999) Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Trans Softw Eng 25: 651\u2013660","journal-title":"IEEE Trans Softw Eng"},{"key":"152_CR15","unstructured":"Symbolic analysis laboratory SAL http:\/\/sal.csl.sri.com\/"},{"key":"152_CR16","doi-asserted-by":"crossref","unstructured":"Steiner W, Paulitsch M (2002) The transition from asynchronous to synchronous system operation: an approach for distributed fault-tolerant systems. In: Proceedings of the 22nd international conference on distributed computing systems (ICDCS\u201902), IEEE Computer Society, p 329","DOI":"10.1109\/ICDCS.2002.1022270"},{"key":"152_CR17","unstructured":"van Hoesel L, Havinga P (2004) A lightweight medium access protocol (LMAC) for wireless sensor networks: reducing preamble transmissions and transceiver state switches. In: Proceedings of 1st international workshop on networked sensing systems (INSS), pp 205\u2013208"},{"key":"152_CR18","unstructured":"Wang QG, Ye Z, Cai WJ, Hang CC (2008) PID control for multivariable processes. Lecture Notes in Control and Information Sciences. Springer, Berlin, p 329"},{"key":"152_CR19","unstructured":"Ye F, Chen A, Lu S, Zhang L, Chen FYA (2001) A scalable solution to minimum cost forwarding in large sensor networks. In: IEEE 10th international conference on computer communications and networks, pp 304\u2013309"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0152-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-011-0152-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0152-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T02:33:44Z","timestamp":1560220424000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-011-0152-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,24]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["152"],"URL":"https:\/\/doi.org\/10.1007\/s11334-011-0152-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,24]]}}}