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

Feng Tan, Yufei Wang, Qixin Wang, Lei Bu, Rong Zheng, Neeraj Suri

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

12 Citations (Scopus)

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.
Original languageEnglish
Title of host publication2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2013
DOIs
Publication statusPublished - 9 Sept 2013
Event2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2013 - Budapest, Hungary
Duration: 24 Jun 201327 Jun 2013

Conference

Conference2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2013
Country/TerritoryHungary
CityBudapest
Period24/06/1327/06/13

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approach'. Together they form a unique fingerprint.

Cite this