{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:17:00Z","timestamp":1743059820600,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216676"},{"type":"electronic","value":"9783319216683"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_25","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T11:08:53Z","timestamp":1436785733000},"page":"429-448","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems"],"prefix":"10.1007","author":[{"given":"Ankush","family":"Desai","sequence":"first","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[]},{"given":"David","family":"Broman","sequence":"additional","affiliation":[]},{"given":"John C.","family":"Eidson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"25_CR1","unstructured":"15.4e 2012. IEEE standard for local and metropolitan area networks-part 15.4: Low-rate wireless personal area networks (LR-WPANs) amendment 1: MAC sublayer (2012)"},{"key":"25_CR2","volume-title":"The Algorithmic Analysis of Hybrid Systems.Theoretical Computer Science","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The Algorithmic Analysis of Hybrid Systems.Theoretical Computer Science. Kluwer Academic Publisher, The Netherlands (1995)"},{"key":"25_CR3","volume-title":"A Theory of Timed Automata.Theoretical Computer Science","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A Theory of Timed Automata.Theoretical Computer Science. Kluwer Academic Publishers, The Netherlands (1994)"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-540-27813-9_42","volume-title":"Computer Aided Verification","author":"T Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: a model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484\u2013487. Springer, Heidelberg (2004)"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Berry, G., Ramesh, S., Shyamasundar, R.: Communicating reactive processes. In: Proceedings of POPL (1993)","DOI":"10.1145\/158511.158526"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Broman, D., Derler, P., Desai, A., Eidson, J.C., Seshia, S.A.: Endlessly circulating messages in IEEE 1588\u20132008 systems. In: Proceedings of the 8th International IEEE Symposium on Precision Clock Synchronization for Measurement, Control and Communication (ISPCS), September 2014","DOI":"10.21236\/ADA605335"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-45416-0_21","volume-title":"Computer Safety, Reliability and Security","author":"P Caspi","year":"2001","unstructured":"Caspi, P., Mazuet, C., Reynaud Paligot, N.: About the design of distributed control systems: the quasi-synchronous approach. In: Voges, U. (ed.) SAFECOMP 2001. LNCS, vol. 2187, p. 215. Springer, Heidelberg (2001)"},{"key":"25_CR8","unstructured":"Corbett, J.C., Dean, J., Epstein, M., Fikes, A., Frost, C., Furman, J.J., Ghemawat, S., Gubarev, A., Heiser, C., Hochschild, P., Hsieh, W., Kanthak, S., Kogan, E., Li, H., Lloyd, A., Melnik, S., Mwaura, D., Nagle, D., Quinlan, S., Rao, R., Rolig, L., Saito, Y., Szymaniak, M., Taylor, C., Wang, R., Woodford, D.: Spanner: google\u2019s globally-distributed database. In: Proceedings of OSDI (2012)"},{"key":"25_CR9","unstructured":"Daws, C., Yovine, S.: Two examples of verification of multirate timed automata with Kronos. In: Proceedings of RTSS (1995)"},{"key":"25_CR10","unstructured":"Desai, A., Broman, D., Eidson, J., Qadeer, S., Seshia, S.A.: Approximate synchrony: An abstraction for distributed time-synchronized systems. Technical report UCB\/EECS-2014-136, University of California, Berkeley, June 2014"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Desai, A., Gupta, V., Jackson, E.K., Qadeer, S., Rajamani, S.K., Zufferey, D.P.: Safe asynchronous event-driven programming. In: Proceedings of PLDI (2013)","DOI":"10.1145\/2491956.2462184"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.: Approximate synchrony: An abstraction for distributed almost-synchronous systems. Technical report UCB\/EECS-2015-158, EECS Department, University of California, Berkeley, May 2015","DOI":"10.1007\/978-3-319-21668-3_25"},{"issue":"1","key":"25_CR13","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/7531.7533","volume":"34","author":"D Dolev","year":"1987","unstructured":"Dolev, D., Dwork, C., Stockmeyer, L.: On the minimal synchronism needed for distributed consensus. J. ACM 34(1), 77\u201397 (1987)","journal-title":"J. ACM"},{"issue":"2","key":"25_CR14","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM 35(2), 288\u2013323 (1988)","journal-title":"J. ACM"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Emmi, M., Qadeer, S., Rakamari\u0107, Z.: Delay-bounded scheduling. In: Proceedings of POPL (2011)","DOI":"10.1145\/1926385.1926432"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Bioinformatics)","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-68413-8_2","volume-title":"Formal Methods in Systems Biology","author":"J Fisher","year":"2008","unstructured":"Fisher, J., Henzinger, T.A., Mateescu, M., Piterman, N.: Bounded asynchrony: concurrency for modeling cell-cell interactions. In: Fisher, J. (ed.) FMSB 2008. LNCS (LNBI), vol. 5054, pp. 17\u201332. Springer, Heidelberg (2008)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"25_CR18","unstructured":"Halbwachs, N., Mandel, L.: Simulation and verification of asynchronous systems by means of a synchronous model. In: Proceedings of ACSD (2006)"},{"key":"25_CR19","unstructured":"Huang, X., Singh, A., Smolka, S.A.: Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol. In: Proceedings of NFM (2010)"},{"key":"25_CR20","unstructured":"IEEE Instrumentation and Measurement Society. IEEE Standard for a Precision Clock Synchronization Protocol for Networked Measurement and Control Systems (2008)"},{"issue":"1\u201312","key":"25_CR21","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. STTT 1(1\u201312), 134\u2013152 (1997)","journal-title":"Int. J. STTT"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Lipinski, M., Wlostowski, T., Serrano, J., Alvarez, P., Gonzalez Cobas, J., Rubini, A., Moreira, P.: Performance results of the first white rabbit installation for cngs time transfer. In: Proceedings of ISPCS (2012)","DOI":"10.1109\/ISPCS.2012.6336610"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of PLDI (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Perlman, R.: An algorithm for distributed computation of a spanning tree in an extended LAN. In: Proceedings of SIGCOMM (1985)","DOI":"10.1145\/319056.319004"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-56188-9_9","volume-title":"Distributed Algorithms","author":"S Ponzio","year":"1992","unstructured":"Ponzio, S., Strong, R.: Semisynchrony and real time. In: Segall, A., Zaks, S. (eds.) Distributed Algorithms. Lecture Notes in Computer Science, vol. 647, pp. 120\u2013135. Springer, Berlin Heidelberg (1992)"},{"key":"25_CR26","unstructured":"Rajan, B., Shyamasundar, R.: Multiclock esterel: a reactive framework for asynchronous design. In: IPDPS (2000)"},{"key":"25_CR27","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.adhoc.2005.01.002","volume":"3","author":"B Sundararaman","year":"2005","unstructured":"Sundararaman, B., Buy, U., Kshemkalyani, A.D.: Clock synchronization for wireless sensor networks: a survey. Ad Hoc Netw. 3, 281\u2013323 (2005). (Elsevier, 2005)","journal-title":"Ad Hoc Netw."},{"key":"25_CR28","series-title":"Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-17994-5_14","volume-title":"Ad Hoc Networks","author":"A Tinka","year":"2010","unstructured":"Tinka, A., Watteyne, T., Pister, K.: A decentralized scheduling algorithm for time synchronized channel hopping. In: Zheng, J., Simplot-Ryl, D., Leung, V.C.M. (eds.) ADHOCNETS 2010. LNICST, vol. 49, pp. 201\u2013216. Springer, Heidelberg (2010)"},{"issue":"4","key":"25_CR29","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s00165-006-0008-1","volume":"18","author":"FW Vaandrager","year":"2006","unstructured":"Vaandrager, F.W., de Groot, A.: Analysis of a biphase mark protocol with Uppaal and PVS. Formal Aspects Comput. 18(4), 433\u2013458 (2006)","journal-title":"Formal Aspects Comput."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:16:13Z","timestamp":1563826573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}