CPS Project (NSF)

CPS now is a new emerging research area that include a wide range of related disciplines with different approaches, methods, tools and experimental platforms. This project is looking into one of the branch in this broad area: Monitoring.

The growing complexity of modern engineered systems,and their increased reliance on computation, calls for novel approaches to guaranteeing their correct functioning. This is especially important for automotive systems where a failure can have catastrophic consequences.

One way to ensure correctness of acomplex system is to thoroughly test and/or verify it. While testing can increase condence in a component, it can not guarantee correctness. Verication, on the other hand, can guarantee correctness, but it is simply not feasible, for example, for a car with advanced engine controls and numerous networked microprocessors. In other cases, the component might have been veried for correctness on a model which was not accurate. And more importantly, even if acomponent is found to be defective through verication,we may still want to use it if the incorrect behavior only occurs rarely.

Runtime monitoring of the behavior of a component is an approach that can complement testing and verication. It can provide another layer of safety to the operation of the system. The monitor observes the inputs and outputs of the component and checks whether the behavior of the system is consistent with the expected behavior. Monitors can be especially useful if a fail-safe shut down procedures can be developed, which is true for abroad class of systems. We propose that monitor design be separate from the system design and be performed after the design of the system by a different set of designers. The fundamental advantage of monitors is that they are inprinciple easy to design and implement, and they do not fundamentally constrain the design of acomponent. Such two layer approach ensures that incorrect behaviors, due to potential faulty component designs, are detected by the monitor and are acted upon.

Investigators:

Principal Investigator(s) : Prof. Prasad Sistla

CoPrincipal Investigator(s) : Prof. Milos Zefran

Graduate student(s) : Yao Feng; Andrey Yavolovsky

Support: NSF Award number 1035914

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.

This project proposes monitoring techniques, for checking the correctness of system behavior during it’s operation, and raising an alarm when the system seems to exhibit erroneous behavior, which can be acted on. Hybrid automata are employed to describe both system behavior whose behavior is probabilistic in it’s evolution due to uncertainties introduced by noise and other factors and the property to be monitored which is specified on system behavior. Monitoring such systems is a challenging problem as the monitor can not observe the system state, but can only observe the outputs generated by it.

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.

We have so far given exact characterizations of when a system is monitorable with respect to a property and is strongly monitorable with respect to a property. For cases when a system is monitorable with respect to a property, we have developed monitoring techniques that can obtain arbitrarily high levels of accuracy close to 1. These techniques were implemented and were shown to be effective using some examples. In order to implement the monitors, we have developed estimation techniques for hybrid systems based on particle filters. Due to its highly nonlinear(the discrete jumping evolution), particle filter shows its advantage in the state estimation. Since the experimental system has several million high-dimensional hybrid states, so by using Rao-Blackwellization, it’s possible to reduce the dimension while resampling is performed to get higher accuracy with less particles, also Kalman filters are used for continuous variables for a better performance.

Based on the findings we have so far, some refined and new ideas are to be implemented:

• Development of cost based metrics for optimizing monitors;
• Development of techniques based on Partially Observable Markov Decision Pocesses (POMDPs) to generate optimal policies for monitoring safety as well as liveness properties and investigate the effect of different reward structures on the accuracy of the monitoring;
• Investigation on monitoring technique when the property automaton is based on expected values.

Conference Papers and Presentations:

• Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan (2015). Decidable and Expressive classes of Probabilistic Automata.  18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015).
• Noohi, E. and Parastegari, S. and Zefran, M. (2015). Computational model for dyadic and bimanual reaching movements. 2015 {IEEE} World Haptics Conference (WHC).
• Jiang, Wen and Žefran, M. (2015). Location control for information dissemination. American Control Conference (ACC), 2015.
• Eugenio, Barbara Di and Žefran, Miloš (2015). The RoboHelper Project: From Multimodal Corpus to Embodiment on a Robot. 2015 AAAI Fall Symposium Series.
• Javaid, Maria and Zefran, Milos and Yavolovsky, Andrey (2015). Using pressure sensors to identify manipulation actions during human physical interaction. 2015 24th IEEE International Symposium on Robot and Human Interactive Communication (RO-MAN).
• A. Prasad Sistla, K. Gondi, V. Venkatakrishnan (2014). DEICS: Data Erasure In Concurrent Software. The 19th Nordic Conference on Secure IT Systems (NordSec 2014). Tromsø, Norway.

• Richard Meyer, Fabian Just, Raymond A. DeCarlo, Milos Zefran, and Meeko Oishi (2014). Notch Filter and MPC for Powered Wheelchair Operation Under Parkinson’s Tremor. 2014 American Control Conference (ACC). Portland, Oregon, USA.

• Scott C. Johnson, Raymond A. DeCarlo , and Milos Zefran (2014). Set-transition observability of switched linear systems. American Control Conference (ACC), 2014. Portland, OR, USA.

• A. Prasad Sistla, M. Zefran, Y. Feng, Y. Ben (2014). Timely Monitoring in Partially Observable Stochastic Systems. 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014). Berlin, Germany.

• Wen Jiang and Milos Zefran (2013). Coverage control with information aggregation. IEEE Conference on Decision and Control. Florence, Italy.

• Soumya Banerjee, Kai Da Zhao, Wenjing Rao, and Milos Zefran (2013). Decentralized Self-balancing Systems. Very Large Scale Integration (VLSI-SoC). Istanbul.

• A. Prasad Sistla, Milos Zefran and Yao Feng, Monitorability of Stochastic Dynamic Systems, Proceedings of the 23rd International Conference on Computer Aided Verification, (2011).

• Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan, Model Checking Concurrent Programs with Nondeterminism and Randomization, Proceedings of the 30th Annual FSTTCS (Foundations of Software Technology and Theoretical Computer Science) Conference, 2010, Chennai, India.

Journal Publications:

• Chen, Lin and Javaid, Maria and Di Eugenio, Barbara and Žefran, Miloš (2015). The roles and recognition of Haptic-Ostensive actions in collaborative multimodal human–human dialogues.  Computer Speech & Language. 34 (1),  201–231.
• Sistla, A. Prasad, Ouri Wolfson, and Bo Xu. “Continuous nearest-neighbor queries with location uncertainty.” The VLDB Journal (2014): 1-26.

• Dragut, Eduard, Hong Wang, Prasad Sistla, Clement Yu, and Weiyi Meng. “Polarity Consistency Checking for Domain Independent Sentiment Dictionaries.” (2014)

• Richard T. Meyer, Miloš Žefran, and Raymond A. DeCarlo (2014). A Comparison of the Embedding Method With Multiparametric Programming, Mixed-Integer Programming, Gradient-Descent, and Hybrid Minimum Principle-Based Methods.  IEEE Transactions on Control Systems Technology. 22 (5),  1784 – 1800

• S. Wei, K. Uthaichana, M. Zefran, R. DeCarlo (2013). Hybrid Model Predictive Control for the Stabilization of Wheeled Mobile Robots Subject to Wheel Slippage.  IEEE Transactions on Control Systems Technology. 21 (6),  2181 – 2193

• Kasemsak Uthaichana, Raymond DeCarlo, Sorin Bengea, Milos Zefran, and Steve Pekarek, Hybrid optimal theory and predictive control for power management in hybrid electric vehicle, Journal of Nonlinear Systems and Applications, (2011), In Press.
  

• Carlos H. Caicedo-Nunez and Milos Zefran, Distributed Task Assignment in Mobile Sensor Networks, IEEE Transactions on Automatic Control, (2011), In Press.

Thesis/Dissertations:

• Serra, Eric. Complexity of Monitors for Cyber-Physical Systems and their Implementation on a Mobile Robot. (2015).  University of Illinois at Chicago.
• Balteri, Ruggero. Modular Design of Monitors for Cyber-Physical Systems from Formal Specifications. (2015).  University of Illinois at Chicago.