More Web Proxy on the site http://driver.im/

research-article

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

Authors:

Sandeep K. S. GuptaAuthors Info & Claims

ICCPS '13: Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems

Pages 71 - 80

https://doi.org/10.1145/2502524.2502535

Published: 08 April 2013 Publication History

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

References

[1]

K. A. Aalborg, K. E. Andersen, and M. Hjbjerre. A Bayesian Approach to Bergman's Minimal Model. In in: C. M. Bishop, B. J. Frey (Eds.), Proceedings of the Ninth International Workshop on Artificial Intelligence, 2003.

[2]

H. Alt, J. Blőmer, and H. Wagener. Approximation of convex polygons. In M. Paterson, editor, Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 703--716. Springer Berlin/Heidelberg, 1990.

Digital Library

[3]

A. Banerjee and S. K. S. Gupta. Appendix for ICCPS 2013. http://impact.asu.edu/BanerjeeICCPSApp.pdf.

[4]

A. Banerjee and S. K. S. Gupta. Your mobility can be injurious to your health: Analyzing pervasive health monitoring systems under dynamic context changes. In IEEE International Conference on Pervasive Computing and Communications (PerCom), pages 39--47, march 2012.

[5]

A. Banerjee, S. Kandula, T. Mukherjee, and S. K. S. Gupta. Band-aide: A tool for cyber-physical oriented analysis and design of body area networks and devices. ACM Trans. Embed. Comput. Syst., 11(S2):49:1--49:29, aug 2012.

Digital Library

[6]

E. Bartocci, F. Corradini, M. R. Di Berardini, E. Entcheva, R. Grosu, and S. A. Smolka. Spatial Networks of Hybrid I/O Automata for Modeling Excitable Tissue. Electronic Notes in Theoretical Computer Science (ENTCS'08), 194(3):51--67.

Digital Library

[7]

D. Bleecker and G. Csordas. Basic Partial Differential Equations. Chapman and Hall, 1995.

[8]

M. C. Bujorianu. An integrated specification logic for cyber-physical systems. In ICECCS 2009, pages 291--300.

Digital Library

[9]

C. Cortazar, M. Elgueta, and J. D. Rossi. A nonlocal diffusion equation whose solutions develop a free boundary. Annales Henri Poincare, 6:269--281, 2005.

[10]

G. Frehse. Phaver: Algorithmic verification of hybrid systems past hytech. In HSCC, pages 258--273, 2005.

Digital Library

[11]

R. Ghosh and C. Tomlin. A query-based technique for interpreting reachable sets for hybrid automaton models of protein feedback signaling. In Proceedings of the American Control Conference, pages 4417--4422, June 2005.

[12]

A. Girard and C. Guernic. Zonotope/hyperplane intersection for hybrid systems reachability analysis. In Proceedings of the 11th international workshop on Hybrid Systems: Computation and Control, HSCC '08, pages 215--228, Berlin, Heidelberg, 2008. Springer-Verlag.

Digital Library

[13]

S. Graf and W. Zhang, editors. Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006, volume 4218 of Lecture Notes in Computer Science. Springer, 2006.

Digital Library

[14]

D. G. M. Greenhalgh, M. B. R. Lawless, B. B. Chew, W. A. Crone, M. E. Fein, and T. L. M. Palmieri. Temperature threshold for burn injury: An oximeter safety study. Journal of Burn Care and Rehabilitation, 25(5):411--415, 2004.

[15]

N. Grégoire and M. Bouillot. Hausdorff distance between convex polygons. http://cgm.cs.mcgill.ca/godfried/teaching/cg-projects/98/normand/main.html.

[16]

T. L. Jackson and H. M. Byrne. A mathematical model to study the effects of drug resistance and vasculature on the response of solid tumors to chemotherapy. Mathematical Biosciences, 164(1):17--38, 2000.

[17]

K.-D. Kim, S. Mitra, and P. R. Kumar. Bounded ε-reach set computation of a class of deterministic and transversal linear hybrid automata. CoRR, abs/1205.3426, 2012.

[18]

A. Lamperski and A. Ames. On the existence of zeno behavior in hybrid systems with non-isolated zeno equilibria. In Decision and Control, 2008. CDC 2008. 47th IEEE Conference on, pages 2776--2781, dec. 2008.

[19]

J. Lee, S. Bohacek, J. Hespanha, and K. Obraczka. Modeling communication networks with hybrid systems. Networking, IEEE/ACM Transactions on, 15(3):630--643, June 2007.

Digital Library

[20]

NSF. Program solicitation. http://www.nsf.gov/pubs/2011/nsf11516/nsf11516.htm.

[21]

H. H. Pennes. Analysis of tissue and arterial blood temperature in the resting human forearm. In Journal of Applied Physiology, volume 1.1, pages 93--122, 1948.

[22]

A. Schafer and M. John. Conceptional Modeling and Analysis of Spatio-Temporal Processes in Biomolecular Systems. In S. Link and M. Kirchberg, editors, Sixth Asia-Pacific Conference on Conceptual Modelling (APCCM 2009), volume 96 of CRPIT, pages 39--48, Wellington, New Zealand, 2009.

Digital Library

[23]

C. Sinem, E. Mustafa, and K. T. John. Lifetime analysis of a sensor network with hybrid automata modelling. In WSNA '02: Proceedings of the 1st ACM international workshop on Wireless sensor networks and applications, pages 98--104, New York, NY, USA.

Digital Library

[24]

Q. Tang, N. Tummala, S. K. S. Gupta, and L. Schwiebert. Communication scheduling to minimize thermal effects of implanted biosensor networks in homogeneous tissue. Biomedical Engineering, IEEE Transactions on, 52(7):1285--1294, July 2005.

[25]

Q. Tang, N. Tummala, S. K. S. Gupta, and L. Schwiebert. TARA: thermal-aware routing algorithm for implanted sensor networks. Lecture Notes in Computer Science, 3560:206--217, 2005.

Digital Library

[26]

The Networking Information Technology Research and Development Program. Different definition of cyber physical systems.

[27]

A. Tiwari. Hybridsal relational abstracter. In P. Madhusudan and S. Seshia, editors, Computer Aided Verification, volume 7358 of Lecture Notes in Computer Science, pages 725--731. Springer Berlin Heidelberg, 2012.

Digital Library

[28]

Q. Yong, W. Ying-Jie, and J. Li-Min. Hybrid cellular automata model for railway transportation system and its implementation on GIS. In Intelligent Vehicles Symposium, pages 543--546, June 2003.

Cited By

Pan SWang CXie WLu JHuang QZuo Z(2024)Modeling and Verification Methods for Spatio-Temporal Consistency of CPS in Uncertain EnvironmentsIEEE Transactions on Reliability10.1109/TR.2024.338470273:4(1849-1862)Online publication date: Dec-2024
https://doi.org/10.1109/TR.2024.3384702
Yang WXu CPan MZhou YHuang Z(2023)Ensure: Towards Reliable Control of Cyber-Physical Systems Under UncertaintyIEEE Transactions on Reliability10.1109/TR.2022.316711672:1(289-301)Online publication date: Mar-2023
https://doi.org/10.1109/TR.2022.3167116
Parnianifard AZemouche AChancharoen RImran MWuttisittikulkij L(2020)Robust optimal design of FOPID controller for five bar linkage robot in a Cyber-Physical System: A new simulation-optimization approachPLOS ONE10.1371/journal.pone.024261315:11(e0242613)Online publication date: 30-Nov-2020
https://doi.org/10.1371/journal.pone.0242613
Show More Cited By

Index Terms

Spatio-temporal hybrid automata for safe cyber-physical systems: a medical case study
1. Theory of computation
  1. Formal languages and automata theory

Recommendations

Spatio-Temporal Event Model for Cyber-Physical Systems
ICDCSW '09: Proceedings of the 2009 29th IEEE International Conference on Distributed Computing Systems Workshops

The emerging Cyber-Physical Systems (CPSs) are envisioned to integrate computation, communication and control with the physical world. Therefore, CPS requires close-interactions between the cyber and physical worlds both in time and space. These ...
Cyber-Physical Systems: Integrated Computing and Engineering Design
Modeling Automotive Cyber Physical Systems
DCABES '13: Proceedings of the 2013 12th International Symposium on Distributed Computing and Applications to Business, Engineering & Science

Automotive cyber physical systems (CPSs) involve interactions between software controllers, communication networks, and physical devices. These systems are among the most complex cyber physical systems being designed by humans. However, automotive cyber ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCPS '13: Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems

April 2013

278 pages

ISBN:9781450319966

DOI:10.1145/2502524

General Chair:
Chenyang Lu
Washington University
,
Program Chairs:
P. R. Kumar
Texas A&M University
,
R. Stoleru
Texas A&M University

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

IEEE-CS\TCRT: TC on Real-Time Systems
SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 April 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

ICCPS '13

Sponsor:

IEEE-CS\TCRT
SIGBED

ICCPS '13: ACM/IEEE 4th International Conference on Cyber-Physical Systems

April 8 - 11, 2013

Pennsylvania, Philadelphia

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
181
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Pan SWang CXie WLu JHuang QZuo Z(2024)Modeling and Verification Methods for Spatio-Temporal Consistency of CPS in Uncertain EnvironmentsIEEE Transactions on Reliability10.1109/TR.2024.338470273:4(1849-1862)Online publication date: Dec-2024
https://doi.org/10.1109/TR.2024.3384702
Yang WXu CPan MZhou YHuang Z(2023)Ensure: Towards Reliable Control of Cyber-Physical Systems Under UncertaintyIEEE Transactions on Reliability10.1109/TR.2022.316711672:1(289-301)Online publication date: Mar-2023
https://doi.org/10.1109/TR.2022.3167116
Parnianifard AZemouche AChancharoen RImran MWuttisittikulkij L(2020)Robust optimal design of FOPID controller for five bar linkage robot in a Cyber-Physical System: A new simulation-optimization approachPLOS ONE10.1371/journal.pone.024261315:11(e0242613)Online publication date: 30-Nov-2020
https://doi.org/10.1371/journal.pone.0242613
Cheng A(2019)Work-in-Progress: Simplifying CPS Development with Real-Time Virtual Resources2019 IEEE Real-Time Systems Symposium (RTSS)10.1109/RTSS46320.2019.00065(564-567)Online publication date: Dec-2019
https://doi.org/10.1109/RTSS46320.2019.00065
Graja IKallel SGuermouche NCheikhrouhou SHadj Kacem A(2019)Modelling and verifying time-aware processes for cyber-physical environmentsIET Software10.1049/iet-sen.2018.503413:1(36-48)Online publication date: 1-Feb-2019
https://doi.org/10.1049/iet-sen.2018.5034
Gatouillat ABadr YMassot BSejdic E(2018)Internet of Medical Things: A Review of Recent Contributions Dealing With Cyber-Physical Systems in MedicineIEEE Internet of Things Journal10.1109/JIOT.2018.28490145:5(3810-3822)Online publication date: Oct-2018
https://doi.org/10.1109/JIOT.2018.2849014
Kruglova TYaroshenko IRabotalov N(2018)Cyber-Physical System of Intelligent Diagnosis of Generator Winding Insulation2018 International Conference on Industrial Engineering, Applications and Manufacturing (ICIEAM)10.1109/ICIEAM.2018.8728883(1-6)Online publication date: May-2018
https://doi.org/10.1109/ICIEAM.2018.8728883
Graja IKallel SGuermouche NKacem A(2018)Verification of the Consistency of Time-Aware Cyber-Physical ProcessesService-Oriented Computing – ICSOC 2017 Workshops10.1007/978-3-319-91764-1_6(67-79)Online publication date: 16-Jun-2018
https://doi.org/10.1007/978-3-319-91764-1_6
Graja IKallel SGuermouche NCheikhrouhou SHadj Kacem A(2018)A comprehensive survey on modeling of cyber‐physical systemsConcurrency and Computation: Practice and Experience10.1002/cpe.485032:15Online publication date: 18-Oct-2018
https://doi.org/10.1002/cpe.4850
Jin WLiu ZShi ZJin CLee J(2017)CPS-enabled worry-free industrial applications2017 Prognostics and System Health Management Conference (PHM-Harbin)10.1109/PHM.2017.8079208(1-7)Online publication date: Jul-2017
https://doi.org/10.1109/PHM.2017.8079208
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents