Creating An Integrated Modular Environment for the Modelling, Analysis and Verification of Embedded Hybrid Systems

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

Abstract Embedded hybrid systems are ubiquitous throughout society: industrial machines, automobiles, medical equipment, household appliances, airplanes, power grids, and environmental monitoring systems all fall under their rubric. The mission-critical nature of the applications in which embedded hybrid systems are used demands high levels of efficiency, performance, reliability, safety, and security. Furthermore, there is an increasingly critical need for the tight integration of multiple applications developed using diverse design paradigms such as periodic feedback control, human interfaces, information processing, and intelligent autonomy to reduce system size, weight, and power consumption. The safety and security of information differs vastly from the safety and security of control. Most industrial control systems used to operate utilities and factories are linked to the Internet, and have wireless sensor networks that can be compromised with a laptop, wireless card, and directional antennae. In an information technology system, security measures are designed around protecting critical core servers, while security of individual remote terminals is not prioritized. However, in the control of an actual physical hybrid system, remote programmable logic controllers (PLCs), which remotely control a facility's sensors and actuators via wireless means, play a key role: If the supervisory control system is compromised, the threat is not as great as if a PLC is attacked. Simply encrypting transmissions and passwords does not provide the solution, and often compromises safety. Hence, an entirely different architecture for designing, implementing, and verifying security in hybrid control systems is necessary. To address these challenges, a tightly integrated design, analysis, verification, and implementation environment for real-time, safe, and security-critical embedded hybrid systems is being created. It includes a formalism-independent method for embedded hybrid system architectural specification with attributes and semantics for verification and validation of properties such as security and safety, along with mechanisms that allow for the composition of models specified in different hybrid modeling languages in a secure and safe manner. More specifically, an abstract functional interface will be created to enhance modularity of the developed solution techniques and reward structures will be used to perform directed searches of a state space to mitigate the state explosion problem. In addition, backwards reachability techniques will be used in order to find escape paths from hazardous states, thereby mitigating the number of states that need to be explored, rendering the problem of verification and validation more tractable. Meshing these two approaches promises to yield groundbreaking results in the scale and complexity of hybrid systems that can be modeled, analyzed, and verified. The broader goal of the project is to produce an industrial-strength tool for the modeling, analysis, and verification of hybrid systems for initial distribution to research institutions, and, upon refinement, to interested industrial partners, such as utilities and airlines. The project will also help create a multidisciplinary base of students (both graduate and undergraduate) from diverse fields such as computer science, operations management, and systems engineering who are competent in the modeling, analysis, and verification of large, complex systems. The result will be an enhanced safety and security culture in academia and industry, which will create overt awareness of the field in the students who will be tomorrow's engineers. It will thus lead to a revolution in the way that complex systems are designed.