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, automotive and many other applications. Since
verification of correctness, in general, is infeasible and testing is not
exhaustive, it is of critical importance to monitor such system during their
operation and detect erroneous behaviors to be acted on.
Monitoring techniques are investigated, when the system state is not fully observable, it's behavior is stochastic and the property to be monitored is specified on the system trajectory. Theoretically, two notions called monitorability and strong monitorability are difined and the necessary and sufficient conditions characterizing them are also given. General monitoring techniques for cases when systems are modeled as stochastic hybrid automata, and the properties are specified as safety or liveness automata are presented State estimation is another key step in the monitoring, since the property is defined on system behavior which is hidden and partial observable. Rao-Blackwellised Particle Filtering is employed in this hybrid state framework.
When exploring a scalar field, for example, concentration
of oil spill over Mexico Gulf, by a group of sensors, it is always a
question that where to deploy them over the area of interest. In general,
the deployment of the sensors satisfies our demand, such as covering the
whole area of interest.
In our project, we need more sensors to cover the part where the amount of information over that part is higher than others. Thus, we need an index for every point over the area of interest to quantify information density. In our research, We found that curvature is a good choice to quantify the information density of the field. By definition, curvature of a surface describes the amount by which the surface deviates from being a flat plane. At a certain point, the higher the curvature is, the more sharply the surface bends. Accordingly, the higher information density that point has. Since curvature is a function of the field, i.e., it can not be read directly from the sensors, we estimate it from the splines which approximate the field. Moreover, all sensors are mobile ones. So, a step-by-step motion algorithm should be embedded to drive them to an optimal sensing configuration, which means within each sensor's region of responsibility, the integral of the curvature, i.e., the amount of the information, should be the same.
It's easy to reach optimal deployment given there is a central server that collects sensor readings and positions of all sensor nodes. Nevertheless, We want to make our task a distributed one which is more challenging. In our problem settings, we assume that there is no central server, each sensor node decides where to move based on the information only provided by its instant neighbors.
So, there are two key problems for us. The first one is how to approximate the field by splines. Once we know the field, we may compute the curvature via the field. The second one is based on local information, where each sensor should move to achieve the global optimization deployment.
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 infinite 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 gave 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 some examples
Support: NSF grant IIS-0093581 and UIC Campus Research Board