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