File preview
Tackling New Frontiers in Modeling and Analysis of Cyber-Physical Systems
Ayan Banerjee and Sandeep K.S. Gupta
IMPACT Lab, School of Computing Informatics and Decision Systems Engineering, Arizona State University, Tempe, Az, Email: {abanerj3, sandeep.gupta}@asu.edu
Computing System Computing Requirements 1. Reliability 2. Accuracy 3. Throughput 4. Latency 5. Safety Physical System Physical Requirements Multi-dimensional 1. Safety Partial Differential 2. Energy Equations efficiency Dynamic contexts 3. Low carbon Random footprint Processes Continuous physical process
Abstract—With the advent of smart sensors and actuators, computing units are interacting with the physical environment at a much larger scale than ever before, through feedback and controlled actuation. Such cyber-physical systems (CPSes) are by definition mission critical and have strict requirements on safety, security, sustainability, reliability, and long term sustainable operation. Guaranteeing these requirements needs accurate understandings of the large scale complex interactions of the computing units with the physical environment and an inter-disciplinary approach towards problem solving in several domains such as control systems, hybrid systems, and operating systems. Common assumptions of linearity, time invariance, dimensionality, non-emergent behavior are no longer applicable. This paper presents some outcomes of NSF funded CPS projects to illustrate inapplicability of existing mathematical tools to characterize CPS behavior with desired accuracy, and new frontiers in theoretical and practical computer science that have to be overcome in order to design CPSes with the desired guarantees on requirements.
Control Algorithm
Actuator
Sensor Unintended Side Effects
Control Algorithm
Cyber-Physical Interactions (CPI)
SpatioTemporal
Aggregate Effects
Low dimension Determinism
Dynamic Contexts
Simplifying Assumptions
Linearity Time Invariance
Independence of Computation & Physics
Ignore emergent behavior
Fig. 1. System model of cyber-physical systems showing the characteristics of aggregate effects and common assumptions for modeling and analysis.
I. Introduction Advances in mobile sensing and embedded computing has enabled pervasive applications, where computing units are interacting with the physical environment not only through monitoring and decision making in the computing domain, but also through critical control operations on the physical properties of the environment, including human physiology [1]. Termed as Cyber-Physical Systems (CPSes), to emphasize the close coupling of computation and physics, such systems have to satisfy strict requirements on safety, security, reliability and long term sustainable operations [2], since a faulty operation or a sub-optimal design can lead to grave consequences including loss of revenue and life. A CPS, thus undergoes mandatory requirements verification in both pre and post implementation phases before marketing or deployment. A popular methodology for pre-implementation requirements verification is modelbased analysis, that represents a CPS using suitable abstractions and then analyzes the system properties using theoretical proofs or simulations. This paper identifies key assumptions in recent works on model-based requirements verification of CPSes, and evaluates the validity of such assumptions under large scale cyber-physical interactions. At a very high level, a CPS can be modeled as a network of embedded computing units (Figure 1) which interact with their physical environment through sensing of physical parameters, e.g., blood glucose level in human, actuation of a control strategy, e.g., infusion of correct amount of insulin to control the blood glucose level, and unintended side effects, e.g., destroying healthy cells in addition to cancer cells through
chemotherapy. The computing unit runs a discrete control algorithm, while the physical system is modeled using mathematical formulations. For the sake of a focused discussion, we will consider an Artificial Pancreas (AP) [3], used for insulin infusion to control blood glucose level in humans, (discussed in Section II) as examplar CPS in this paper. Historically, CPS modeling and design started with considering reactive control systems. The execution of such systems were driven by the discrete time decision of the computing unit while physical dynamics could be modeled with linear state space equations [4]. This enabled the usage of standard control system tools with the related assumptions of linearity and time invariance for analysis of CPSes with reasonable accuracy. However, soon the design of CPSes evolved into more complex ones where feedback from the physical environment caused events in the computing domain according to which the control actions had to change. In case of an AP system whenever the glucose concentration decreases below a low threshold value (hypo-glycemia) the infusion pump goes into a braking state, decreasing the infusion rate [1]. The execution of the system were now governed by the dynamics in the physical environment. Notions of discrete states controlled by continuous dynamics asked for hybrid modeling and researchers came up with hybrid systems/automata [5] that can effectively capture the interactions and theoretically prove CPS safety, security, sustainability, and reliability properties. Both control system and hybrid system based solutions have efficient methods and strong results under the assumption of linearity and time invariance. With recent advances, AP systems are becoming proactive using predictive models of human physiology to estimate the
glucose concentration in the future given the current physiological state [3]. Such predictions are used as feedback to drive the execution of the system. These predictive models are non-linear, time delayed, and often consider a spatio-temporal variation of physical parameters. Verifying such AP systems with hybrid automata requires approximating the complex predictive models using linear ones. This reduces accuracy of the requirements verification results. Further, hybrid systems only consider events generated by the continuous dynamics. Formerly, there has been limited focus on considering the discrete random events along with events generated by continuous dynamics in the same hybrid automata model. For example, hybrid systems simultaneously modeling a computing mode change due to low glucose concentration event, which is governed by the continuous physical dynamics and a random patient bolus request event are hard to analyze and have not been studied in sufficient details. Such drawbacks can soon render currently available analysis tools inapplicable due to their oversimplifications. This paper identifies the key assumptions that need to be revisited in order to strengthen currently available theories and tools for performing model-based analysis and verification of CPSes at the required level of accuracy. The paper discusses the research outcomes of NSF funded projects (CNS #0831544 and IIS #1116385) awarded to IMPACT Lab ASU using a specific example of Artificial Pancreas. It also identifies key focus areas for future research and education in order to invoke cyber-physical thinking among researchers. The results of the discussion are summarized in the form of a course outline and associated educational outcomes available online at: http: //impact.asu.edu/CPSCourseOutline.html. II. Example CPS - Artificial Pancreas Artificial pancrea [1] (AP) is a good example of cyberphysical systems. An AP system consists of a discrete controller, which gets feedback from the human glycemic dynamics through a continuous glucose monitor (CGM) and determines the amount of insulin infusion needed to keep the blood glucose concentration at a certain level. The insulin is then injected by an insulin pump attached to the body. The control algorithm has three modes: a) braking, where the basal rate is continually adjusted based on the hypoglycemic risk levels, b) meal supervision, where a bolus infusion is delivered whenever the user has a meal intake, and c) correction bolus, which is invoked when the glucose level is greater than a safe value (250 mg/dl) and the infusion rate is increased according to the predicted glucose level 1hr ahead in time. In general, control algorithms in CPSes can be far more complex [3]. However, even this simple example leads to violation of important assumptions that make tractable analysis and simulation of CPS a hard challenge. A. Cyber-physical interaction The cyber-physical interactions in this example CPS mainly arise from the physiological feedback to the control algorithm. This feedback could be a reading of blood glucose levels from a glucose meter or an estimation using a pharmacokinetic
model of insulin-glucose interaction. Such cyber-physical interactions can be characterized in several granularities of space and time each having its own assumptions and accuracy. Linear time delay model: One of the oldest form of the pharmacokinetic model represented different organs of the body using state variables. The time variation of each variable is expressed as a function of other variables through a set of linear differential equation. To model the transport delays for the drug to reach different parts of the body, the state variables are often time delayed. High accuracy in simulating such models of interaction requires potentially infinite number of states as discussed in Section III. Non-linear model: Often instead of the drug pharmacokinetics a more important aspect is the interaction between insulin and glucagon. The Bergman’s minimal model [6] is a well established method of representing such interactions. However, the model is non-linear due to the negative feedback effect of insulin on glucose concentration. This is expressed by a differential equation where the rate of change of glucose concentration is a function of the product of glucose and insulin concentration. Spatio-temporal model: To accurately characterize the spatiotemporal drug diffusion dynamics complex pharmacokinetics represent the drug concentration as a linear second order partial differential equation (PDE) over space and time [7]. The coefficients of the PDE vary over time depending on the physiological and mental state of the subject. Absence of Emergent behavior: In cases when two drugs are infused simultaneously for example insulin and glucagon, the effect of interacting drugs may not be obtain by simple combination of the effects of individual drugs. In fact emergent behavior is often expected, which may not be characterized using any closed form mathematical model. III. Assumptions violated Characterization of cyber-physical interactions introduce several complexities in the mathematical representation of the CPS. In this section, we enlist a few of the assumptions of commonly used theories that make them unsuitable for large scale cyber-physical interactions. A. Linearity: A popular assumption in control system analysis is linearity and time invariance of dynamics (Figure 1). A comprehensive theory for controllability, observability, and stability exist for linear time invariant (LTI) systems. Theories such as Laplace transforms for continuous domain, z transforms for discrete domain, root locus theory all work under the simplifying assumption of linearity i.e., the temporal variation of any continuous variable x controlled by the controller is governed by a linear ordinary differential equation (ODE). In case of cyber-physical interactions such theories have to be abandoned more often than not. Non-linearities in the physical dynamics for CPSes can arise in several forms. For example, in case of AP systems (Section II), the Bergman model [6] expresses the rate of change of glucose concentra˙ tion G(t) as a function of the product of G(t) and I(t). Further, non-linearities can arise in the form of power laws as in the
case of Penne’s bioheat equation [8], if we consider Stefan’s law for radiation based heat transfer. B. Time invariance: Since an LTI system has well established theories for analysis and proving properties, a first attempt to characterize any CPS is to use the time invariance assumption (Figure 1). However, such an assumption is not always true. For example in case of infusion pumps administering chemotherapy, the drug diffusion coefficient changes with time as the cells in a particular region die. The cell death rate is expressed using a partial differential equation whose coefficients are varying over time introducing time variance. C. Low dimensionality: Typically systems are analyzed over one time dimension. However, cyber-physical interactions occur over both space and time; concentration of infused insulin is more near the infusion site. Such spatio-temporal variations (Figure 1) increase the dimensionality of the problem from one time dimension to four time and space dimensions. Often it suffices to discretize the space dimension into points of interest, which in turn increase the number of state variables. Moreover, when time delays are considered in CPS, then matters get complicated. For the linear time delay pharmacokinetic models, the insulin concentration I(t) is a function of its past values I(t−T i ), where T i is a transport delay. In such cases, for continuous evaluation of I(t), one needs all possible values of I from t to t − T i , requiring an infinite number of states thus increasing the dimensionality. D. Determinism: Deterministic systems are preferred by researchers since its execution can be traced with certainty. However, cyber-physical interactions have a high degree of non-determinism. In the AP example, the meal supervision module is activated depending on the meal intake by the user. The meal intake process cannot be characterized using any deterministic model. Thus, if the glucose concentration is high the controller may transit to two different states: a) meal supervision or b) correction bolus. Such systems can only be analyzed when some model of randomness is incorporated, which aggravates the complexity of analysis. E. Independence of algorithm and physical dynamics: The close coupling of computing operation and physical dynamics in CPSes have led to the usage of Hybrid Automata [5] for analysis. An important factor in control algorithms is the user input, which is typically random in nature. However, a hybrid automata is primarily designed to handle events that are generated by continuous evolution of the system and hence are predictable. Random events such as meal intake for AP systems may not be analyzed simultaneously with events in the continuous domain using available algorithms. Hence the usage of hybrid automata is based on the assumption of independence between the random events in the algorithm of computing units and events occurring due to continuous evolution of the system. F. Emergent behavior: Emergent behavior are typically difficult to model in CPSes. For multi-drug infusion in chemotherapy [9], the emergent behavior is characterized by simultaneously solving two sets of interdependent partial differential equations with time varying coefficients. Solutions to such systems are complex and may often lack closed form represen-
tation. Estimations with finite error are the only approach that currently exist in literature to tackle emergent behavior. Infinite precision characterization of emergent behavior is needed for providing guarantees on properties of CPS. IV. Survey of solutions and educational outcomes This section discusses several potential solutions to overcome the assumptions mentioned in Section III. A. Mathematical implications of physical models Models of cyber-physical interactions range from the most basic linear time domain differential equations [4] to complex spatio-temporal non-linear time invariant partial differential equations [9]. With so many available model it is essential to choose the right model for the right purpose. Outcome 1: Which model to choose? This requires an intricate balance between complexity and accuracy. For analgesic infusion pumps with a reactive control systems it suffices to just use a linear state space model of drug diffusion [4]. However, for model predictive control systems which use non-linear models such as Bergman’s model as a predictor, a linear model of diffusion is not justified since the requirements verifier uses a model that is less accurate than the controller. For an appropriately chosen model there exist several solution techniques each having its own assumptions on initial and boundary conditions. Outcome 2: What are the mathematical implications of the chosen model? A linear state space model has a solution with infinite precision. A non-linear model such as Bergman’s minimal model of glucose and insulin interaction does not have a closed form solution. Thus, the requirements verification results has to account for the finite error in estimating the glucose or insulin concentration. Further, the characteristics of the physical environment plays an important role in the solution methodology. Typically partial differential equations have closed form solutions with infinite precision when there is a fixed boundary condition. However, diffusion dynamics in humans does not have fixed boundaries and hence the models representing such dynamics should be solved as a free boundary problem [7]. Such problems do not typically have closed form solutions and thus there is a need to perform error analysis of the verification results. B. Combining models of computation The execution of the AP systems considered in the project are governed by random discrete events (meal supervision) in the computing domain as well as events caused by continuous variation of physical parameters (low glucose concentration or hypoglycemia). The computing domain events are typically modeled using Finite State Machines (FSMs) while the physical domains events are modeled using hybrid automata (HA). Such separation of concerns is not applicable for CPSes such as APs. In this regard, a possible approach is to interface the different models of computation in a meaningful way so that they can be theoretically analyzed for CPS properties. Outcome 3: How to compose different models of computation? A possible way to compose formal models is to develop
hierarchies. For example, a finite state machine can be used to describe the discrete random events of an AP. Each state of the FSM can employ a hybrid system to model the events in the physical domain. Such hierarchical automata are proposed [10] but there has been limited progress in their simulation or theoretical proofs and is still a topic of active research. C. Spatio-temporal considerations Consideration of spatio-temporal dynamics increases the number of independent dimensions in the problem from just one, time dimension, to four, one time and three space dimensions. Such high dimensionality causes several problems for accurate requirement verification of CPSes. Outcome 4: How to tackle spatio-temporal variations in a fast and accurate way? Traditionally spatial dynamics has been tackled using a discretization approach, Finite Difference Time Domain (FDTD). The space is discretized into grids and each grid point has fixed temporal dynamics [11]. Such specifications are fast to simulate but are not suitable for characterizing emergent behavior of CPSes [7]. Especially for a hybrid system, this entails changing the dynamics from linear time domain ordinary differential equations to spatiotemporal partial differential equations. Theoretical analysis of hybrid systems with partial differential equation (PDE) has only been studied very recently [7], which defines a spatiotemporal hybrid automata (STHA) and is achievable only for one time and one space dimension. D. Characterizing emergent behavior Emergent behavior as discussed in Section III can only be characterized with finite error, by solving simultaneous spatiotemporal PDEs. This assumes that we know exactly at what time and what space point the emergent behavior occurs. Such exact estimation of the time and space point of emergent effects has not been considered in sufficient details. Outcome 5: How to compute occurrences of emergent effects and estimate its magnitude? Recent research have expressed emergent effects as an aggregation of effects of individual computing units in a CPS in some mathematical form [9]. For example, in case of chemotherapy with multiple drugs emergent effects are obtained by simultaneously solving interdependent partial differential equations. Researchers have shown that a STHA can automatically compute the space and time of occurrence of emergent behavior if some model of the emergence is assumed [7]. Such theories characterizing emergent behavior is essential for requirements verification of CPSes and has received recent attention [7], [12], [13]. E. Randomized analysis The randomness in CPSes requires a stochastic approach towards verification. Randomness including irregular meal patterns in AP systems and mobility of user may cause serious violation of requirements such as safety [13]. CPS modeling and analysis should thus focus on stochastic evaluation of systems for requirements verification. Outcome 6: How to provide guarantees under stochastic assumptions? In response to this need, researchers have recently
focused on stochastic hybrid automata and its analysis for proving system properties [14]. However, for such solutions the execution time scales exponentially with problem size. V. Conclusions Based on the outcomes discussed in Section IV we propose a graduate level research course on modeling and analysis of cyber-physical systems and also discuss its educational outcomes(http://impact.asu.edu/CPSCourseOutline.html). The course will introduce researchers to advanced topics in nonlinear control systems and time variant state space solutions, topics in non-linear partial differential equations and solving under different boundary conditions, formal methods including spatio-temporal hybrid automata and stochastic reachability analysis, and theory of emergence and chaos. The course will encourage researchers to relax the common assumptions and develop novel solutions to hard theoretical and practical problems in CPS design and analysis. References
[1] B. Kovatchev, S. Patek, E. Dassau, F. Doyle, L. Magni, G. D. Nicolao, and C. Cobelli, “Control to range for diabetes: Functionality and modular architecture,” Journal of diabetes Science and Technology, 2012. [2] The Networking Information Technology Research and Development Program, “Different definition of cyber physical systems.” [Online]. Available: http://www.nitrd.gov/about/blog/white papers/ 16-Importance of Cyber-Physical Systems.pdf [3] S. D. Patek, L. Magni, E. Dassau, C. Hughes-Krvetski, C. Toffanin, G. DeNicolao, S. D. Favero, M. Breton, C. D. Man, E. Renard, H. Zisser, F. J. Doyle, C. Cobelli, and B. P. Kovatchev, “Modular closed-loop control of diabetes,” IEEE Transaction on Biomedical Engineering, vol. 59, no. 11, pp. 2986–2999, nov 2012. [4] D. R. Wada and D. S. Ward, “The hybrid model: a new pharmacokinetic model for computer-controlled infusion pumps,” Biomedical Engineering, IEEE Transactions on, vol. 41, no. 2, pp. 134 –142, feb. 1994. [5] T. A. Henzinger, “The theory of hybrid automata,” Logic in Computer Science, Symposium on, vol. 0, p. 278, 1996. [6] 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.), Proc. of the 9th International Workshop on Artificial Intelligence,, 2003. [7] A. Banerjee and S. K. S. Gupta, “Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study,” Intl’ Conf’ on Cyber-Physical Systems (Accepted for Publication), April 2013. [8] H. H. Pennes, “Analysis of tissue and arterial blood temperature in the resting human forearm,” in Journal of Applied Physiology, vol. 1.1, 1948, pp. 93–122. [9] 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, vol. 164, no. 1, pp. 17 – 38, 2000. [10] E. Mikk, Y. Lakhnechi, and M. Siegel, Hierarchical automata as model for statecharts. Lecture Notes in Computer Science : Advances in Computing Science ASIAN’97, 1997. [11] 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), vol. 194, no. 3, pp. 51–67, 2008. [12] A. Banerjee, S. Kandula, T. Mukherjee, and S. K. S. Gupta, “Bandaide: A tool for cyber-physical oriented analysis and design of body area networks and devices,” ACM Trans. Embedded Comput. Syst., vol. 11, no. S2, p. 49, 2012. [13] 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 Pervasive Computing and Communications (PerCom), IEEE International Conference on, march 2012, pp. 39 –47. [14] M. Prandini and J. Hu, “Application of reachability analysis for stochastic hybrid systems to aircraft conflict prediction,” in 47th IEEE Conference on Decision and Control,, dec. 2008, pp. 4036 –4041.
Ayan Banerjee and Sandeep K.S. Gupta
IMPACT Lab, School of Computing Informatics and Decision Systems Engineering, Arizona State University, Tempe, Az, Email: {abanerj3, sandeep.gupta}@asu.edu
Computing System Computing Requirements 1. Reliability 2. Accuracy 3. Throughput 4. Latency 5. Safety Physical System Physical Requirements Multi-dimensional 1. Safety Partial Differential 2. Energy Equations efficiency Dynamic contexts 3. Low carbon Random footprint Processes Continuous physical process
Abstract—With the advent of smart sensors and actuators, computing units are interacting with the physical environment at a much larger scale than ever before, through feedback and controlled actuation. Such cyber-physical systems (CPSes) are by definition mission critical and have strict requirements on safety, security, sustainability, reliability, and long term sustainable operation. Guaranteeing these requirements needs accurate understandings of the large scale complex interactions of the computing units with the physical environment and an inter-disciplinary approach towards problem solving in several domains such as control systems, hybrid systems, and operating systems. Common assumptions of linearity, time invariance, dimensionality, non-emergent behavior are no longer applicable. This paper presents some outcomes of NSF funded CPS projects to illustrate inapplicability of existing mathematical tools to characterize CPS behavior with desired accuracy, and new frontiers in theoretical and practical computer science that have to be overcome in order to design CPSes with the desired guarantees on requirements.
Control Algorithm
Actuator
Sensor Unintended Side Effects
Control Algorithm
Cyber-Physical Interactions (CPI)
SpatioTemporal
Aggregate Effects
Low dimension Determinism
Dynamic Contexts
Simplifying Assumptions
Linearity Time Invariance
Independence of Computation & Physics
Ignore emergent behavior
Fig. 1. System model of cyber-physical systems showing the characteristics of aggregate effects and common assumptions for modeling and analysis.
I. Introduction Advances in mobile sensing and embedded computing has enabled pervasive applications, where computing units are interacting with the physical environment not only through monitoring and decision making in the computing domain, but also through critical control operations on the physical properties of the environment, including human physiology [1]. Termed as Cyber-Physical Systems (CPSes), to emphasize the close coupling of computation and physics, such systems have to satisfy strict requirements on safety, security, reliability and long term sustainable operations [2], since a faulty operation or a sub-optimal design can lead to grave consequences including loss of revenue and life. A CPS, thus undergoes mandatory requirements verification in both pre and post implementation phases before marketing or deployment. A popular methodology for pre-implementation requirements verification is modelbased analysis, that represents a CPS using suitable abstractions and then analyzes the system properties using theoretical proofs or simulations. This paper identifies key assumptions in recent works on model-based requirements verification of CPSes, and evaluates the validity of such assumptions under large scale cyber-physical interactions. At a very high level, a CPS can be modeled as a network of embedded computing units (Figure 1) which interact with their physical environment through sensing of physical parameters, e.g., blood glucose level in human, actuation of a control strategy, e.g., infusion of correct amount of insulin to control the blood glucose level, and unintended side effects, e.g., destroying healthy cells in addition to cancer cells through
chemotherapy. The computing unit runs a discrete control algorithm, while the physical system is modeled using mathematical formulations. For the sake of a focused discussion, we will consider an Artificial Pancreas (AP) [3], used for insulin infusion to control blood glucose level in humans, (discussed in Section II) as examplar CPS in this paper. Historically, CPS modeling and design started with considering reactive control systems. The execution of such systems were driven by the discrete time decision of the computing unit while physical dynamics could be modeled with linear state space equations [4]. This enabled the usage of standard control system tools with the related assumptions of linearity and time invariance for analysis of CPSes with reasonable accuracy. However, soon the design of CPSes evolved into more complex ones where feedback from the physical environment caused events in the computing domain according to which the control actions had to change. In case of an AP system whenever the glucose concentration decreases below a low threshold value (hypo-glycemia) the infusion pump goes into a braking state, decreasing the infusion rate [1]. The execution of the system were now governed by the dynamics in the physical environment. Notions of discrete states controlled by continuous dynamics asked for hybrid modeling and researchers came up with hybrid systems/automata [5] that can effectively capture the interactions and theoretically prove CPS safety, security, sustainability, and reliability properties. Both control system and hybrid system based solutions have efficient methods and strong results under the assumption of linearity and time invariance. With recent advances, AP systems are becoming proactive using predictive models of human physiology to estimate the
glucose concentration in the future given the current physiological state [3]. Such predictions are used as feedback to drive the execution of the system. These predictive models are non-linear, time delayed, and often consider a spatio-temporal variation of physical parameters. Verifying such AP systems with hybrid automata requires approximating the complex predictive models using linear ones. This reduces accuracy of the requirements verification results. Further, hybrid systems only consider events generated by the continuous dynamics. Formerly, there has been limited focus on considering the discrete random events along with events generated by continuous dynamics in the same hybrid automata model. For example, hybrid systems simultaneously modeling a computing mode change due to low glucose concentration event, which is governed by the continuous physical dynamics and a random patient bolus request event are hard to analyze and have not been studied in sufficient details. Such drawbacks can soon render currently available analysis tools inapplicable due to their oversimplifications. This paper identifies the key assumptions that need to be revisited in order to strengthen currently available theories and tools for performing model-based analysis and verification of CPSes at the required level of accuracy. The paper discusses the research outcomes of NSF funded projects (CNS #0831544 and IIS #1116385) awarded to IMPACT Lab ASU using a specific example of Artificial Pancreas. It also identifies key focus areas for future research and education in order to invoke cyber-physical thinking among researchers. The results of the discussion are summarized in the form of a course outline and associated educational outcomes available online at: http: //impact.asu.edu/CPSCourseOutline.html. II. Example CPS - Artificial Pancreas Artificial pancrea [1] (AP) is a good example of cyberphysical systems. An AP system consists of a discrete controller, which gets feedback from the human glycemic dynamics through a continuous glucose monitor (CGM) and determines the amount of insulin infusion needed to keep the blood glucose concentration at a certain level. The insulin is then injected by an insulin pump attached to the body. The control algorithm has three modes: a) braking, where the basal rate is continually adjusted based on the hypoglycemic risk levels, b) meal supervision, where a bolus infusion is delivered whenever the user has a meal intake, and c) correction bolus, which is invoked when the glucose level is greater than a safe value (250 mg/dl) and the infusion rate is increased according to the predicted glucose level 1hr ahead in time. In general, control algorithms in CPSes can be far more complex [3]. However, even this simple example leads to violation of important assumptions that make tractable analysis and simulation of CPS a hard challenge. A. Cyber-physical interaction The cyber-physical interactions in this example CPS mainly arise from the physiological feedback to the control algorithm. This feedback could be a reading of blood glucose levels from a glucose meter or an estimation using a pharmacokinetic
model of insulin-glucose interaction. Such cyber-physical interactions can be characterized in several granularities of space and time each having its own assumptions and accuracy. Linear time delay model: One of the oldest form of the pharmacokinetic model represented different organs of the body using state variables. The time variation of each variable is expressed as a function of other variables through a set of linear differential equation. To model the transport delays for the drug to reach different parts of the body, the state variables are often time delayed. High accuracy in simulating such models of interaction requires potentially infinite number of states as discussed in Section III. Non-linear model: Often instead of the drug pharmacokinetics a more important aspect is the interaction between insulin and glucagon. The Bergman’s minimal model [6] is a well established method of representing such interactions. However, the model is non-linear due to the negative feedback effect of insulin on glucose concentration. This is expressed by a differential equation where the rate of change of glucose concentration is a function of the product of glucose and insulin concentration. Spatio-temporal model: To accurately characterize the spatiotemporal drug diffusion dynamics complex pharmacokinetics represent the drug concentration as a linear second order partial differential equation (PDE) over space and time [7]. The coefficients of the PDE vary over time depending on the physiological and mental state of the subject. Absence of Emergent behavior: In cases when two drugs are infused simultaneously for example insulin and glucagon, the effect of interacting drugs may not be obtain by simple combination of the effects of individual drugs. In fact emergent behavior is often expected, which may not be characterized using any closed form mathematical model. III. Assumptions violated Characterization of cyber-physical interactions introduce several complexities in the mathematical representation of the CPS. In this section, we enlist a few of the assumptions of commonly used theories that make them unsuitable for large scale cyber-physical interactions. A. Linearity: A popular assumption in control system analysis is linearity and time invariance of dynamics (Figure 1). A comprehensive theory for controllability, observability, and stability exist for linear time invariant (LTI) systems. Theories such as Laplace transforms for continuous domain, z transforms for discrete domain, root locus theory all work under the simplifying assumption of linearity i.e., the temporal variation of any continuous variable x controlled by the controller is governed by a linear ordinary differential equation (ODE). In case of cyber-physical interactions such theories have to be abandoned more often than not. Non-linearities in the physical dynamics for CPSes can arise in several forms. For example, in case of AP systems (Section II), the Bergman model [6] expresses the rate of change of glucose concentra˙ tion G(t) as a function of the product of G(t) and I(t). Further, non-linearities can arise in the form of power laws as in the
case of Penne’s bioheat equation [8], if we consider Stefan’s law for radiation based heat transfer. B. Time invariance: Since an LTI system has well established theories for analysis and proving properties, a first attempt to characterize any CPS is to use the time invariance assumption (Figure 1). However, such an assumption is not always true. For example in case of infusion pumps administering chemotherapy, the drug diffusion coefficient changes with time as the cells in a particular region die. The cell death rate is expressed using a partial differential equation whose coefficients are varying over time introducing time variance. C. Low dimensionality: Typically systems are analyzed over one time dimension. However, cyber-physical interactions occur over both space and time; concentration of infused insulin is more near the infusion site. Such spatio-temporal variations (Figure 1) increase the dimensionality of the problem from one time dimension to four time and space dimensions. Often it suffices to discretize the space dimension into points of interest, which in turn increase the number of state variables. Moreover, when time delays are considered in CPS, then matters get complicated. For the linear time delay pharmacokinetic models, the insulin concentration I(t) is a function of its past values I(t−T i ), where T i is a transport delay. In such cases, for continuous evaluation of I(t), one needs all possible values of I from t to t − T i , requiring an infinite number of states thus increasing the dimensionality. D. Determinism: Deterministic systems are preferred by researchers since its execution can be traced with certainty. However, cyber-physical interactions have a high degree of non-determinism. In the AP example, the meal supervision module is activated depending on the meal intake by the user. The meal intake process cannot be characterized using any deterministic model. Thus, if the glucose concentration is high the controller may transit to two different states: a) meal supervision or b) correction bolus. Such systems can only be analyzed when some model of randomness is incorporated, which aggravates the complexity of analysis. E. Independence of algorithm and physical dynamics: The close coupling of computing operation and physical dynamics in CPSes have led to the usage of Hybrid Automata [5] for analysis. An important factor in control algorithms is the user input, which is typically random in nature. However, a hybrid automata is primarily designed to handle events that are generated by continuous evolution of the system and hence are predictable. Random events such as meal intake for AP systems may not be analyzed simultaneously with events in the continuous domain using available algorithms. Hence the usage of hybrid automata is based on the assumption of independence between the random events in the algorithm of computing units and events occurring due to continuous evolution of the system. F. Emergent behavior: Emergent behavior are typically difficult to model in CPSes. For multi-drug infusion in chemotherapy [9], the emergent behavior is characterized by simultaneously solving two sets of interdependent partial differential equations with time varying coefficients. Solutions to such systems are complex and may often lack closed form represen-
tation. Estimations with finite error are the only approach that currently exist in literature to tackle emergent behavior. Infinite precision characterization of emergent behavior is needed for providing guarantees on properties of CPS. IV. Survey of solutions and educational outcomes This section discusses several potential solutions to overcome the assumptions mentioned in Section III. A. Mathematical implications of physical models Models of cyber-physical interactions range from the most basic linear time domain differential equations [4] to complex spatio-temporal non-linear time invariant partial differential equations [9]. With so many available model it is essential to choose the right model for the right purpose. Outcome 1: Which model to choose? This requires an intricate balance between complexity and accuracy. For analgesic infusion pumps with a reactive control systems it suffices to just use a linear state space model of drug diffusion [4]. However, for model predictive control systems which use non-linear models such as Bergman’s model as a predictor, a linear model of diffusion is not justified since the requirements verifier uses a model that is less accurate than the controller. For an appropriately chosen model there exist several solution techniques each having its own assumptions on initial and boundary conditions. Outcome 2: What are the mathematical implications of the chosen model? A linear state space model has a solution with infinite precision. A non-linear model such as Bergman’s minimal model of glucose and insulin interaction does not have a closed form solution. Thus, the requirements verification results has to account for the finite error in estimating the glucose or insulin concentration. Further, the characteristics of the physical environment plays an important role in the solution methodology. Typically partial differential equations have closed form solutions with infinite precision when there is a fixed boundary condition. However, diffusion dynamics in humans does not have fixed boundaries and hence the models representing such dynamics should be solved as a free boundary problem [7]. Such problems do not typically have closed form solutions and thus there is a need to perform error analysis of the verification results. B. Combining models of computation The execution of the AP systems considered in the project are governed by random discrete events (meal supervision) in the computing domain as well as events caused by continuous variation of physical parameters (low glucose concentration or hypoglycemia). The computing domain events are typically modeled using Finite State Machines (FSMs) while the physical domains events are modeled using hybrid automata (HA). Such separation of concerns is not applicable for CPSes such as APs. In this regard, a possible approach is to interface the different models of computation in a meaningful way so that they can be theoretically analyzed for CPS properties. Outcome 3: How to compose different models of computation? A possible way to compose formal models is to develop
hierarchies. For example, a finite state machine can be used to describe the discrete random events of an AP. Each state of the FSM can employ a hybrid system to model the events in the physical domain. Such hierarchical automata are proposed [10] but there has been limited progress in their simulation or theoretical proofs and is still a topic of active research. C. Spatio-temporal considerations Consideration of spatio-temporal dynamics increases the number of independent dimensions in the problem from just one, time dimension, to four, one time and three space dimensions. Such high dimensionality causes several problems for accurate requirement verification of CPSes. Outcome 4: How to tackle spatio-temporal variations in a fast and accurate way? Traditionally spatial dynamics has been tackled using a discretization approach, Finite Difference Time Domain (FDTD). The space is discretized into grids and each grid point has fixed temporal dynamics [11]. Such specifications are fast to simulate but are not suitable for characterizing emergent behavior of CPSes [7]. Especially for a hybrid system, this entails changing the dynamics from linear time domain ordinary differential equations to spatiotemporal partial differential equations. Theoretical analysis of hybrid systems with partial differential equation (PDE) has only been studied very recently [7], which defines a spatiotemporal hybrid automata (STHA) and is achievable only for one time and one space dimension. D. Characterizing emergent behavior Emergent behavior as discussed in Section III can only be characterized with finite error, by solving simultaneous spatiotemporal PDEs. This assumes that we know exactly at what time and what space point the emergent behavior occurs. Such exact estimation of the time and space point of emergent effects has not been considered in sufficient details. Outcome 5: How to compute occurrences of emergent effects and estimate its magnitude? Recent research have expressed emergent effects as an aggregation of effects of individual computing units in a CPS in some mathematical form [9]. For example, in case of chemotherapy with multiple drugs emergent effects are obtained by simultaneously solving interdependent partial differential equations. Researchers have shown that a STHA can automatically compute the space and time of occurrence of emergent behavior if some model of the emergence is assumed [7]. Such theories characterizing emergent behavior is essential for requirements verification of CPSes and has received recent attention [7], [12], [13]. E. Randomized analysis The randomness in CPSes requires a stochastic approach towards verification. Randomness including irregular meal patterns in AP systems and mobility of user may cause serious violation of requirements such as safety [13]. CPS modeling and analysis should thus focus on stochastic evaluation of systems for requirements verification. Outcome 6: How to provide guarantees under stochastic assumptions? In response to this need, researchers have recently
focused on stochastic hybrid automata and its analysis for proving system properties [14]. However, for such solutions the execution time scales exponentially with problem size. V. Conclusions Based on the outcomes discussed in Section IV we propose a graduate level research course on modeling and analysis of cyber-physical systems and also discuss its educational outcomes(http://impact.asu.edu/CPSCourseOutline.html). The course will introduce researchers to advanced topics in nonlinear control systems and time variant state space solutions, topics in non-linear partial differential equations and solving under different boundary conditions, formal methods including spatio-temporal hybrid automata and stochastic reachability analysis, and theory of emergence and chaos. The course will encourage researchers to relax the common assumptions and develop novel solutions to hard theoretical and practical problems in CPS design and analysis. References
[1] B. Kovatchev, S. Patek, E. Dassau, F. Doyle, L. Magni, G. D. Nicolao, and C. Cobelli, “Control to range for diabetes: Functionality and modular architecture,” Journal of diabetes Science and Technology, 2012. [2] The Networking Information Technology Research and Development Program, “Different definition of cyber physical systems.” [Online]. Available: http://www.nitrd.gov/about/blog/white papers/ 16-Importance of Cyber-Physical Systems.pdf [3] S. D. Patek, L. Magni, E. Dassau, C. Hughes-Krvetski, C. Toffanin, G. DeNicolao, S. D. Favero, M. Breton, C. D. Man, E. Renard, H. Zisser, F. J. Doyle, C. Cobelli, and B. P. Kovatchev, “Modular closed-loop control of diabetes,” IEEE Transaction on Biomedical Engineering, vol. 59, no. 11, pp. 2986–2999, nov 2012. [4] D. R. Wada and D. S. Ward, “The hybrid model: a new pharmacokinetic model for computer-controlled infusion pumps,” Biomedical Engineering, IEEE Transactions on, vol. 41, no. 2, pp. 134 –142, feb. 1994. [5] T. A. Henzinger, “The theory of hybrid automata,” Logic in Computer Science, Symposium on, vol. 0, p. 278, 1996. [6] 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.), Proc. of the 9th International Workshop on Artificial Intelligence,, 2003. [7] A. Banerjee and S. K. S. Gupta, “Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study,” Intl’ Conf’ on Cyber-Physical Systems (Accepted for Publication), April 2013. [8] H. H. Pennes, “Analysis of tissue and arterial blood temperature in the resting human forearm,” in Journal of Applied Physiology, vol. 1.1, 1948, pp. 93–122. [9] 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, vol. 164, no. 1, pp. 17 – 38, 2000. [10] E. Mikk, Y. Lakhnechi, and M. Siegel, Hierarchical automata as model for statecharts. Lecture Notes in Computer Science : Advances in Computing Science ASIAN’97, 1997. [11] 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), vol. 194, no. 3, pp. 51–67, 2008. [12] A. Banerjee, S. Kandula, T. Mukherjee, and S. K. S. Gupta, “Bandaide: A tool for cyber-physical oriented analysis and design of body area networks and devices,” ACM Trans. Embedded Comput. Syst., vol. 11, no. S2, p. 49, 2012. [13] 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 Pervasive Computing and Communications (PerCom), IEEE International Conference on, march 2012, pp. 39 –47. [14] M. Prandini and J. Hu, “Application of reachability analysis for stochastic hybrid systems to aircraft conflict prediction,” in 47th IEEE Conference on Decision and Control,, dec. 2008, pp. 4036 –4041.