Monitoring Techniques for Safety Critical Cyber-Physical Systems
Abstract:
Correct functioning of cyber-physical systems is of critical importance. This is more so in the case of safety critical systems such as in medical or automotive applications. Since verification of correctness, in general, is infeasible and testing is exhaustive, it is of critical importance to monitor such system during their operation and detect erroneous behaviors to be acted on. The problem of designing monitors for safety critical cyber-physical systems is challenging since the correctness property to be monitored is specified on the probabilistic evolution of system state over time which the monitor cannot directly observe. The probabilities or randomness in the evolution of the system is due to uncertainties introduced by noise or other unpredictable events, such as component failures. The monitor observes the inputs and outputs of the system. By using these information, the monitor needs to decide whether the system execution is correct or not. The project has so far introduced two models for specifying the semantics of such cyber-physical systems. The first model is the Hidden Markov System in which the states of the system are modeled as discrete states after quantization. For such systems the property to be monitored is specified by an automaton on in- finite strings. We defined two accuracy measures of a given monitor – acceptance and rejection accuracies. The accuracies capture percentage of false alarms and missed alarms, respectively. Using these concepts we defined two notions, called strong monitorability and monitorability. We gave exact characterizations when a system is strongly monitorable and monitorable with respect to a property. Based on these notions we developed techniques for monitoring, when the system to be monitored is specified by a probabilistic hybrid automaton and the property to be monitored is given by a deterministic hybrid automaton. We formulated a monitoring method that uses product automaton and estimates probabilities using particle filters. These monitoring techniques are implemented using Matlab and have been shown to be effective on examples. Furthermore, the time complexity of the monitor with respect to safety property is explored. We intro duce a subclass of monitorable systems called exponentially converging monitorable systems. An expression for the expected time for detection of a failure is presented. It’s also shown that strongly monitorable systems and monitorable systems that are bounded and uniform are exponentially converging monitorable. Experimental results show that existing algorithms do exhibit fast convergence when these conditions are satisfied. We have also introduced Extended Hidden Markov Systems (EHMS) where the state of the system is hybrid, i.e., has a continuous state and discrete mode. We extended the monitorability results to the EHMSes. In order to implement monitors suggested by our theoretical analysis, a state estimation algorithm needs to be used. Even if in each discrete mode the cyber-physical system is linear, mode changes (discrete transitions) introduce nonlinearities. Furthermore, systems we consider have a large number of discrete modes, making traditional mode-estimation algorithms difficult to use. In our work we use particle filters to estimate the state of the system; the estimate is in turn used by the monitor. Due to the large discrete modes space, particle depletion represents a particular challenge. Traditionally, depletion calls for increasing number of particles to be used, increasing the computational cost of the particle filter. We use the invariances in the topology of the system stemming from asynchronous transitions to simplify the particle filter and thus dramatically reduce its computational time.
References:
1. A. Sistla, M. Zˇefran, and Y. Feng. Monitorability of stochastic dynamical systems. In Computer Aided Verification, pages 720–736. Springer, 2011
2. A. Sistla, M. Zˇefran, and Y. Feng. Runtime monitoring of stochastic cyber-physical systems with hybrid state. In Runtime Verification, pages 276–293. Springer, 2012
Submitted by Yao Feng
on
Abstract:
Correct functioning of cyber-physical systems is of critical importance. This is more so in the case of safety critical systems such as in medical or automotive applications. Since verification of correctness, in general, is infeasible and testing is exhaustive, it is of critical importance to monitor such system during their operation and detect erroneous behaviors to be acted on. The problem of designing monitors for safety critical cyber-physical systems is challenging since the correctness property to be monitored is specified on the probabilistic evolution of system state over time which the monitor cannot directly observe. The probabilities or randomness in the evolution of the system is due to uncertainties introduced by noise or other unpredictable events, such as component failures. The monitor observes the inputs and outputs of the system. By using these information, the monitor needs to decide whether the system execution is correct or not. The project has so far introduced two models for specifying the semantics of such cyber-physical systems. The first model is the Hidden Markov System in which the states of the system are modeled as discrete states after quantization. For such systems the property to be monitored is specified by an automaton on in- finite strings. We defined two accuracy measures of a given monitor – acceptance and rejection accuracies. The accuracies capture percentage of false alarms and missed alarms, respectively. Using these concepts we defined two notions, called strong monitorability and monitorability. We gave exact characterizations when a system is strongly monitorable and monitorable with respect to a property. Based on these notions we developed techniques for monitoring, when the system to be monitored is specified by a probabilistic hybrid automaton and the property to be monitored is given by a deterministic hybrid automaton. We formulated a monitoring method that uses product automaton and estimates probabilities using particle filters. These monitoring techniques are implemented using Matlab and have been shown to be effective on examples. Furthermore, the time complexity of the monitor with respect to safety property is explored. We intro duce a subclass of monitorable systems called exponentially converging monitorable systems. An expression for the expected time for detection of a failure is presented. It’s also shown that strongly monitorable systems and monitorable systems that are bounded and uniform are exponentially converging monitorable. Experimental results show that existing algorithms do exhibit fast convergence when these conditions are satisfied. We have also introduced Extended Hidden Markov Systems (EHMS) where the state of the system is hybrid, i.e., has a continuous state and discrete mode. We extended the monitorability results to the EHMSes. In order to implement monitors suggested by our theoretical analysis, a state estimation algorithm needs to be used. Even if in each discrete mode the cyber-physical system is linear, mode changes (discrete transitions) introduce nonlinearities. Furthermore, systems we consider have a large number of discrete modes, making traditional mode-estimation algorithms difficult to use. In our work we use particle filters to estimate the state of the system; the estimate is in turn used by the monitor. Due to the large discrete modes space, particle depletion represents a particular challenge. Traditionally, depletion calls for increasing number of particles to be used, increasing the computational cost of the particle filter. We use the invariances in the topology of the system stemming from asynchronous transitions to simplify the particle filter and thus dramatically reduce its computational time.
References:
1. A. Sistla, M. Zˇefran, and Y. Feng. Monitorability of stochastic dynamical systems. In Computer Aided Verification, pages 720–736. Springer, 2011
2. A. Sistla, M. Zˇefran, and Y. Feng. Runtime monitoring of stochastic cyber-physical systems with hybrid state. In Runtime Verification, pages 276–293. Springer, 2012