Cyber-Physical Systems (CPS) tightly integrate computation and communication to control a physical system. Examples of computer-controlled systems include medical devices, airplanes, and automobiles. Such systems are too complex for the designers to completely understand their behavior in every detail. On the other hand, understanding the high-level properties of such systems is of paramount importance since most are safety-critical.
This project seeks to improve model exploration techniques for control systems in two distinct directions. First, it investigates formal languages that partially specify the properties of a system. The goal is to make those specifications more concrete, in a way that they demonstrate what are precisely the properties satisfied by the system. Second, it studies the temporal logic revision problem. Namely, if automatic analysis shows that a desired system specification cannot be satisfied, how can tools propose an alternative specification which can be satisfied and is as close as possible to the originally intended one? The research project will adopt and adapt ideas from temporal logic queries, vacuity and coverage to the CPS setting.
Expected results of the project include tools for (i) the model based exploration of control systems and (ii) the debugging of control system synthesis tools. As a result, the developed techniques will be readily available to designers of embedded control systems to help them explore and better understand their systems. Additionally, the practical and theoretical results of this research will be disseminated to undergraduate and graduate students as well as engineers in local industries through a number of advanced courses and seminars that the PI is teaching.
