Books


Toward Verifying Smart-Health Infrastructure Safety from their Impact on Human Physiology

Paper publications:

Spatio-Temporal Hybrid Automata for Safe Cyber-Physical Systems: A Medical Case Study

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 the interactions are within desired limits. In this project, we proposed a linear 1-space dimension Spatio-Temporal Hybrid Automata (L1STHA) to capture the effects of the interactions, in both time and space. Aggregate effects of interaction in case of concurrent operations in the computing entities are expressed as a set of inter-dependent partial differential equations (PDEs) in dedicated discrete states of the L1STHA model. A time and space bound reachability analysis algorithm is proposed on L1STHAs for safety verification. The reachability analysis provides reachable states of 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 CPSes in the medical domain such as infusion pumps.

Cyber-Physical Systems (CPSes), where computing units interact with the physical environment for either control of the environment or driving computation are becoming increasingly prevalent in the society, especially in healthcare such as infusion pumps. CPSes by definition are safety critical, requiring safety verification before their deployment. As such the need for formal verification to theoretically prove the safety of CPS operation is well recognized.

Formal models for CPSes should capture the following salient features:

  1. Discrete time behavior of the compuing nodes
  2. Continuous dynamics of the physical environment
  3. Spatio-temporal variation of the continuous physical parameters
  4. Aggregate effects from concurrent operations of networked computing nodes

Assumed system model for Cyber-Physical Systems

The L1STHA expresses the variation of system properties according to a discrete control algorithm of the computing units in the CPS.

Conceptual illustration of L1STHA with two modes l1 and l2 and two continuous variables v1 and v2

The L1STHA model of single channel infusion pump

Cyber-physical interactions are the seamless and complex interactions among the computing units and the physical environment in CPSes. Such interactions can be often un-intentional that are harardous to the environment. Many CPSes, are further distributed in nature, i.e. they comprise of network of medical devices controlled through the wireless channel for example multi-channel infusion pumps. The distributed nodes often perform concurrent operations; thus causing aggregation of the detrimental impact on the environment from multiple nodes. Thus, aggregate interactions require proper charactization to ensure the CPS's safety.

The normal and aggregate effect modes in the L1STHA model of multi-channel infusion pumps

A setting of the infusion pump is a tuple with numeric values assigned to five control parameters to perform safety analysis of the infusion pump using the reachability analysis algorithm

  1. control input delay
  2. set point
  3. basal value
  4. sampling interval
  5. infusion increment

Safe and unsafe initial configurations of the infusion pump


Sponsor

This research is funded by NSF grant IIS-1116385.


    Home | Projects | People | Publications | Courses | Resources | Books | News & Visitors | Contact