{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,26]],"date-time":"2025-09-26T13:40:10Z","timestamp":1758894010009,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T00:00:00Z","timestamp":1506470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF 1055094, CNS 1525855"],"award-info":[{"award-number":["CCF 1055094, CNS 1525855"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000161","name":"National Institute of Standards and Technology","doi-asserted-by":"publisher","award":["60NANB16D305, 70NANB16H305"],"award-info":[{"award-number":["60NANB16D305, 70NANB16H305"]}],"id":[{"id":"10.13039\/100000161","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>In order to test the performance and verify the correctness of Cyber-Physical Systems (CPS), the timing constraints on the system behavior must be met. Signal Temporal Logic (STL) can efficiently and succinctly capture the timing constraints of a given system model. However, many timing constraints on CPS are more naturally expressed in terms of events on signals. While it is possible to specify event-based timing constraints in STL, such statements can quickly become long and arcane in even simple systems. Timing constraints for CPS, which can be large and complex systems, are often associated with tolerances, the expression of which can make the timing constraints even more cumbersome using STL. This paper proposes a new logic, Timestamp Temporal Logic (TTL), to provide a definitional extension of STL that more intuitively expresses the timing constraints of distributed CPS. TTL also allows for a more natural expression of timing tolerances. Additionally, this paper outlines a methodology to automatically generate logic code and programs to monitor the expressed timing constraints. Since our TTL monitoring logic evaluates the timing constraints using only the timestamps of the required events on the signal, the TTL monitoring logic has significantly less memory footprint when compared to traditional STL monitoring logic, which stores the signal value at the required sampling frequency. The key contribution of this paper is a scalable approach for online monitoring of the timing constraints. We demonstrate the capabilities of TTL and our methodology for online monitoring of TTL constraints on two case studies: 1) Synchronization and phase control of two generators and, 2) Simultaneous image capture using distributed cameras for 3D image reconstruction.<\/jats:p>","DOI":"10.1145\/3126510","type":"journal-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:33:53Z","timestamp":1506515633000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Timestamp Temporal Logic (TTL) for Testing the Timing of Cyber-Physical Systems"],"prefix":"10.1145","volume":"16","author":[{"given":"Mohammadreza","family":"Mehrabian","sequence":"first","affiliation":[{"name":"Arizona State University, Tempe, AZ, US"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohammad","family":"Khayatian","sequence":"additional","affiliation":[{"name":"Arizona State University, Tempe, AZ, US"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aviral","family":"Shrivastava","sequence":"additional","affiliation":[{"name":"Arizona State University, Tempe, AZ, US"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John C.","family":"Eidson","sequence":"additional","affiliation":[{"name":"University of California Berkeley, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patricia","family":"Derler","sequence":"additional","affiliation":[{"name":"National Instruments corporation, N Mopac Expy, Austin, TX"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hugo A.","family":"Andrade","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, El Cerrito, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ya-Shian","family":"Li-Baboud","sequence":"additional","affiliation":[{"name":"National Institute of Standard and Technology (NIST), Hillsboro, OR"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edward","family":"Griffor","sequence":"additional","affiliation":[{"name":"National Institute of Standard and Technology (NIST), Gaithersburg, MD"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Weiss","sequence":"additional","affiliation":[{"name":"Marc Weiss Consulting, Aptos, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kevin","family":"Stanton","sequence":"additional","affiliation":[{"name":"Intel corporation, Hillsboro, OR"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"The grid code (february 2017) issue 5 revision 20.  The grid code (february 2017) issue 5 revision 20."},{"volume-title":"NIST Cyber Physical Systems Program. https:\/\/www.nist.gov\/programs-projects\/cyber-physical-systems-program. (2016). {Online","year":"2016","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_25"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Johan Bengtsson et al. 1996. UPPAAL - a tool suite for automatic verification of real-time systems. In Hybrid Systems III.   Johan Bengtsson et al. 1996. UPPAAL - a tool suite for automatic verification of real-time systems. In Hybrid Systems III.","DOI":"10.1007\/BFb0020949"},{"volume-title":"Deshmukh et al","year":"2015","author":"Jyotirmoy","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Goran Frehse et al. 2011. SpaceEx: Scalable verification of hybrid systems. In CAV.   Goran Frehse et al. 2011. SpaceEx: Scalable verification of hybrid systems. In CAV.","DOI":"10.1007\/978-3-642-22110-1_30"},{"volume-title":"Henzinger et al","year":"1997","author":"Thomas","key":"e_1_2_1_11_1"},{"volume-title":"IEEE 1588 standard for a precision clock synchronization protocol for networked measurement and control systems","year":"2002","author":"IEEE Instrumentation and Measurement Society","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_2_1_16_1","unstructured":"Oded Maler et al. 2008. Checking temporal properties of discrete timed and continuous behaviors. In Pillars of Computer Science.   Oded Maler et al. 2008. Checking temporal properties of discrete timed and continuous behaviors. In Pillars of Computer Science."},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Oded Maler et al. 2013. Monitoring properties of analog and mixed-signal circuits. International Journal on Software Tools for Technology Transfer 15 (2013).  Oded Maler et al. 2013. Monitoring properties of analog and mixed-signal circuits. International Journal on Software Tools for Technology Transfer 15 (2013).","DOI":"10.1007\/s10009-012-0247-9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1119"},{"volume-title":"AMT: A property-based monitoring tool for analog systems. In FORMATS.","year":"2007","author":"Nickovic Dejan","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2968456.2974012"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3061639.3072955"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126510","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3126510","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3126510","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:01Z","timestamp":1750273501000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126510"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,27]]},"references-count":21,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3126510"],"URL":"https:\/\/doi.org\/10.1145\/3126510","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2017,9,27]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}