Let them be part of our lives

Research focus

The project performs research on ensuring the correct functioning of safety critical cyber physical systems. This is achieved by monitoring the operation of the system at run time. The problem is challenging since the correctness property to be monitored is specified on the evolution of system state over time which the monitor cannot directly observe; furthermore, the evolution of the system is probabilistic. The probabilities or randomness in the evolution of the system is due to uncertainties introduced by noise in the sensors or due to other unpredictable events, such as component failures, modeled probabilistically. The inputs to the monitor are the outputs generatedby the system. These may include some sensor outputs. By using these inputs 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 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.

We have also introduced Extended Hidden Markov Systems (EHMS) in which the state of the system is hybrid, i.e., is a mixture of continuous and discrete. We extended the monitorability results to the EHMSes.

Here, an multi-car train example is shown:

The train system includes two parts: velocity system and braking system. The Fig. 1 and Fig. 2 show its interactive operation principles. With noise disturbing, the velocity would hit the high threshold which leads the start of brakes. For each car, after waiting for some random time when the velocity keeps constant, with small probability 0.1, it goes to failure mode in braking system. Saying we have N cars, since some cars may not succeed to start the brakes, they would be dragged or pushed passively by the other cars, so the physical link force constraint(the constraint comes up with the natural attributes of the material used to connect the two cars) may be violated which would cause the breakage of the train. The other normally behaved cars slow down the velocity until the train hits the low threshold, and again after some random time, bring the system back to its running mode.

Fig. 1   Velocity System

Fig. 2   Braking System

Two properties of the train will be verified: the velocity and the link forces between every neighboring cars. Fig. 3 is the safety property we formalize in the case. As we can see, timers are used in each property to transform the property to safety property.

Fig. 3   Property Automaton

The simply design of monitor is achieved based on the structure of property automaton:

Fig. 4   Monitor


You are here: Home Research focus