Home > Research > Publications & Outputs > Guaranteeing Proper-Temporal-Embedding safety r...

Links

Text available via DOI:

View graph of relations

Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approach

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paper

Published

Standard

Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS : A hybrid formal modeling approach. / Tan, F.; Wang, Y.; Wang, Q.; Bu, L.; Zheng, R.; Suri, Neeraj.

2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, 2013.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paper

Harvard

Tan, F, Wang, Y, Wang, Q, Bu, L, Zheng, R & Suri, N 2013, Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approach. in 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE. https://doi.org/10.1109/DSN.2013.6575357

APA

Tan, F., Wang, Y., Wang, Q., Bu, L., Zheng, R., & Suri, N. (2013). Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approach. In 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN) IEEE. https://doi.org/10.1109/DSN.2013.6575357

Vancouver

Tan F, Wang Y, Wang Q, Bu L, Zheng R, Suri N. Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approach. In 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE. 2013 https://doi.org/10.1109/DSN.2013.6575357

Author

Tan, F. ; Wang, Y. ; Wang, Q. ; Bu, L. ; Zheng, R. ; Suri, Neeraj. / Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS : A hybrid formal modeling approach. 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, 2013.

Bibtex

@inproceedings{d8a2b2c6cb314ae8b6b9519aaf6d722f,
title = "Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approach",
abstract = "Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety critical CPS (control, healthcare etc.) requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE). Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel lease based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal methodology to transform the design pattern hybrid automata into specific wireless CPS designs. This methodology can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct a case study on laser tracheotomy wireless CPS to show that the resulting system is safe and can withstand communication disruptions. {\textcopyright} 2013 IEEE.",
keywords = "Configuration constraints, Continuous-time, Cyber-physical systems (CPS), Design Patterns, Hybrid automatons, Physical world, Safety guarantees, Wireless communications, Communication, Embedded systems, Java programming language, Wireless telecommunication systems, Automata theory",
author = "F. Tan and Y. Wang and Q. Wang and L. Bu and R. Zheng and Neeraj Suri",
year = "2013",
month = jun
day = "24",
doi = "10.1109/DSN.2013.6575357",
language = "English",
isbn = "9781467364713",
booktitle = "2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS

T2 - A hybrid formal modeling approach

AU - Tan, F.

AU - Wang, Y.

AU - Wang, Q.

AU - Bu, L.

AU - Zheng, R.

AU - Suri, Neeraj

PY - 2013/6/24

Y1 - 2013/6/24

N2 - Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety critical CPS (control, healthcare etc.) requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE). Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel lease based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal methodology to transform the design pattern hybrid automata into specific wireless CPS designs. This methodology can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct a case study on laser tracheotomy wireless CPS to show that the resulting system is safe and can withstand communication disruptions. © 2013 IEEE.

AB - Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety critical CPS (control, healthcare etc.) requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE). Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel lease based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal methodology to transform the design pattern hybrid automata into specific wireless CPS designs. This methodology can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct a case study on laser tracheotomy wireless CPS to show that the resulting system is safe and can withstand communication disruptions. © 2013 IEEE.

KW - Configuration constraints

KW - Continuous-time

KW - Cyber-physical systems (CPS)

KW - Design Patterns

KW - Hybrid automatons

KW - Physical world

KW - Safety guarantees

KW - Wireless communications

KW - Communication

KW - Embedded systems

KW - Java programming language

KW - Wireless telecommunication systems

KW - Automata theory

U2 - 10.1109/DSN.2013.6575357

DO - 10.1109/DSN.2013.6575357

M3 - Conference contribution/Paper

SN - 9781467364713

BT - 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)

PB - IEEE

ER -