Timestamp Temporal Logic (TTL) for testing the timing of Cyber-Physical Systems

Mohammadreza Mehrabian, Mohammad Khayatian, Aviral Shrivastava, John C. Eidson, Patricia Derler, Hugo A. Andrade, Ya Shian Li-Baboud, Edward Griffor, Marc Weiss, Kevin Stanton

Research output: Contribution to journalArticle

  • 1 Citations

Abstract

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.

LanguageEnglish (US)
Article number169
JournalACM Transactions on Embedded Computing Systems
Volume16
Issue number5s
DOIs
StatePublished - Sep 1 2017
Externally publishedYes

Fingerprint

Temporal logic
Testing
Monitoring
Cyber Physical System
Phase control
Image reconstruction
Large scale systems
Synchronization
Cameras
Sampling

Keywords

  • CPS
  • Cyber-physical systems
  • Real-time systems
  • Safety critical systems
  • Time testing
  • Timing constraints
  • Verification

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Cite this

Mehrabian, M., Khayatian, M., Shrivastava, A., Eidson, J. C., Derler, P., Andrade, H. A., ... Stanton, K. (2017). Timestamp Temporal Logic (TTL) for testing the timing of Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems, 16(5s), [169]. https://doi.org/10.1145/3126510

Timestamp Temporal Logic (TTL) for testing the timing of Cyber-Physical Systems. / Mehrabian, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Eidson, John C.; Derler, Patricia; Andrade, Hugo A.; Li-Baboud, Ya Shian; Griffor, Edward; Weiss, Marc; Stanton, Kevin.

In: ACM Transactions on Embedded Computing Systems, Vol. 16, No. 5s, 169, 01.09.2017.

Research output: Contribution to journalArticle

Mehrabian, M, Khayatian, M, Shrivastava, A, Eidson, JC, Derler, P, Andrade, HA, Li-Baboud, YS, Griffor, E, Weiss, M & Stanton, K 2017, 'Timestamp Temporal Logic (TTL) for testing the timing of Cyber-Physical Systems' ACM Transactions on Embedded Computing Systems, vol. 16, no. 5s, 169. https://doi.org/10.1145/3126510
Mehrabian, Mohammadreza ; Khayatian, Mohammad ; Shrivastava, Aviral ; Eidson, John C. ; Derler, Patricia ; Andrade, Hugo A. ; Li-Baboud, Ya Shian ; Griffor, Edward ; Weiss, Marc ; Stanton, Kevin. / Timestamp Temporal Logic (TTL) for testing the timing of Cyber-Physical Systems. In: ACM Transactions on Embedded Computing Systems. 2017 ; Vol. 16, No. 5s.
@article{2cac21d7f8984940afe5c7d42e943008,
title = "Timestamp Temporal Logic (TTL) for testing the timing of Cyber-Physical Systems",
abstract = "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.",
keywords = "CPS, Cyber-physical systems, Real-time systems, Safety critical systems, Time testing, Timing constraints, Verification",
author = "Mohammadreza Mehrabian and Mohammad Khayatian and Aviral Shrivastava and Eidson, {John C.} and Patricia Derler and Andrade, {Hugo A.} and Li-Baboud, {Ya Shian} and Edward Griffor and Marc Weiss and Kevin Stanton",
year = "2017",
month = "9",
day = "1",
doi = "10.1145/3126510",
language = "English (US)",
volume = "16",
journal = "ACM Transactions on Embedded Computing Systems",
issn = "1539-9087",
publisher = "Association for Computing Machinery (ACM)",
number = "5s",

}

TY - JOUR

T1 - Timestamp Temporal Logic (TTL) for testing the timing of Cyber-Physical Systems

AU - Mehrabian, Mohammadreza

AU - Khayatian, Mohammad

AU - Shrivastava, Aviral

AU - Eidson, John C.

AU - Derler, Patricia

AU - Andrade, Hugo A.

AU - Li-Baboud, Ya Shian

AU - Griffor, Edward

AU - Weiss, Marc

AU - Stanton, Kevin

PY - 2017/9/1

Y1 - 2017/9/1

N2 - 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.

AB - 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.

KW - CPS

KW - Cyber-physical systems

KW - Real-time systems

KW - Safety critical systems

KW - Time testing

KW - Timing constraints

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=85030695910&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85030695910&partnerID=8YFLogxK

U2 - 10.1145/3126510

DO - 10.1145/3126510

M3 - Article

VL - 16

JO - ACM Transactions on Embedded Computing Systems

T2 - ACM Transactions on Embedded Computing Systems

JF - ACM Transactions on Embedded Computing Systems

SN - 1539-9087

IS - 5s

M1 - 169

ER -