Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Citations (Scopus)

Abstract

Interactions between the computing units and the physical environment in Cyber-Physical Systems (CPSes) are considered to verify safety properties, i.e. ensuring the un-intentional side-effects of cyber-physical interactions are within desired limits. A Linear 1 space dimension Spatio-Temporal Hybrid Automata (L1STHA) is defined to capture the effects of the interactions, in both time and space. Aggregate effects of interactions due to concurrent operations in the computing entities are expressed as a set of interdependent partial differential equations associated with dedicated modes of the L1STHA model. A time and space bound L1STHA reachability analysis algorithm is proposed for safety verification, which provides reachable states of the L1STHA with an arbitrary accuracy e. The runtime of the algorithm depends on the requested accuracy. The usage of the L1STHA modeling and analysis is demonstrated for medical CPSes such as infusion pumps.

Original languageEnglish (US)
Title of host publicationProceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013
Pages71-80
Number of pages10
DOIs
StatePublished - 2013
Event4th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2013 - Philadelphia, PA, United States
Duration: Apr 8 2013Apr 11 2013

Other

Other4th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2013
CountryUnited States
CityPhiladelphia, PA
Period4/8/134/11/13

Fingerprint

Partial differential equations
Pumps
Cyber Physical System

ASJC Scopus subject areas

  • Computer Networks and Communications

Cite this

Banerjee, A., & Gupta, S. (2013). Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study. In Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013 (pp. 71-80) https://doi.org/10.1145/2502524.2502535

Spatio-temporal hybrid automata for safe cyber-physical systems : A medical case study. / Banerjee, Ayan; Gupta, Sandeep.

Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013. 2013. p. 71-80.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Banerjee, A & Gupta, S 2013, Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study. in Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013. pp. 71-80, 4th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2013, Philadelphia, PA, United States, 4/8/13. https://doi.org/10.1145/2502524.2502535
Banerjee A, Gupta S. Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study. In Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013. 2013. p. 71-80 https://doi.org/10.1145/2502524.2502535
Banerjee, Ayan ; Gupta, Sandeep. / Spatio-temporal hybrid automata for safe cyber-physical systems : A medical case study. Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013. 2013. pp. 71-80
@inproceedings{7a8a8f3f37cf4ee7a1f05eabc9220b88,
title = "Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study",
abstract = "Interactions between the computing units and the physical environment in Cyber-Physical Systems (CPSes) are considered to verify safety properties, i.e. ensuring the un-intentional side-effects of cyber-physical interactions are within desired limits. A Linear 1 space dimension Spatio-Temporal Hybrid Automata (L1STHA) is defined to capture the effects of the interactions, in both time and space. Aggregate effects of interactions due to concurrent operations in the computing entities are expressed as a set of interdependent partial differential equations associated with dedicated modes of the L1STHA model. A time and space bound L1STHA reachability analysis algorithm is proposed for safety verification, which provides reachable states of the L1STHA with an arbitrary accuracy e. The runtime of the algorithm depends on the requested accuracy. The usage of the L1STHA modeling and analysis is demonstrated for medical CPSes such as infusion pumps.",
author = "Ayan Banerjee and Sandeep Gupta",
year = "2013",
doi = "10.1145/2502524.2502535",
language = "English (US)",
isbn = "9781450319966",
pages = "71--80",
booktitle = "Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013",

}

TY - GEN

T1 - Spatio-temporal hybrid automata for safe cyber-physical systems

T2 - A medical case study

AU - Banerjee, Ayan

AU - Gupta, Sandeep

PY - 2013

Y1 - 2013

N2 - Interactions between the computing units and the physical environment in Cyber-Physical Systems (CPSes) are considered to verify safety properties, i.e. ensuring the un-intentional side-effects of cyber-physical interactions are within desired limits. A Linear 1 space dimension Spatio-Temporal Hybrid Automata (L1STHA) is defined to capture the effects of the interactions, in both time and space. Aggregate effects of interactions due to concurrent operations in the computing entities are expressed as a set of interdependent partial differential equations associated with dedicated modes of the L1STHA model. A time and space bound L1STHA reachability analysis algorithm is proposed for safety verification, which provides reachable states of the L1STHA with an arbitrary accuracy e. The runtime of the algorithm depends on the requested accuracy. The usage of the L1STHA modeling and analysis is demonstrated for medical CPSes such as infusion pumps.

AB - Interactions between the computing units and the physical environment in Cyber-Physical Systems (CPSes) are considered to verify safety properties, i.e. ensuring the un-intentional side-effects of cyber-physical interactions are within desired limits. A Linear 1 space dimension Spatio-Temporal Hybrid Automata (L1STHA) is defined to capture the effects of the interactions, in both time and space. Aggregate effects of interactions due to concurrent operations in the computing entities are expressed as a set of interdependent partial differential equations associated with dedicated modes of the L1STHA model. A time and space bound L1STHA reachability analysis algorithm is proposed for safety verification, which provides reachable states of the L1STHA with an arbitrary accuracy e. The runtime of the algorithm depends on the requested accuracy. The usage of the L1STHA modeling and analysis is demonstrated for medical CPSes such as infusion pumps.

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

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

U2 - 10.1145/2502524.2502535

DO - 10.1145/2502524.2502535

M3 - Conference contribution

AN - SCOPUS:84883100494

SN - 9781450319966

SP - 71

EP - 80

BT - Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013

ER -