Seminars

What can be formally addressed for industrial control systems? PDF
Xiaoqing Jin, Toyota

9/17/2014, 10:00pm, GHC 9115

Abstract

Hybrid dynamical systems, coupled with sensor networks have had tremendous impacts on every aspects of our daily lives. Concerns of safety, reliability, and efficiency demands researchers to develop new tools and technologies to help analyze such systems. Unfortunately, there is a paucity of standard benchmark systems and accompanying requirements that researchers can use to evaluate and compare the efficacy of their techniques. A closed-loop model of an industrial control system typically involves a plant model describing the dynamical characteristics of the physical processes within the system, and a controller model, which is usually a block-diagram-based representation of the software used to regulate the plant behavior. In practice, industrial-scale plant models and controller models are very complex as they can contain highly nonlinear hybrid dynamics, look-up tables storing pre-computed values, several levels of design-hierarchy, and so on. Moreover, the de facto standard in the automotive and avionics domains is to describe such models in the modeling language Simulink(r). As the formal semantics of Simulink are not public, it makes formal analysis challenging. In this talk, we will present a suite of closed-loop models of powertrain control systems from the automotive domain. These benchmarks are intended to challenge the research community while maintaining a manageable scale. As local requirements amenable to use with verification tools are not typically available, we also present a set of representative requirements specifying the quality of the closed-loop control system.

Biography

Xiaoqing Jin is a senior engineer and researcher at Toyota Technical Center in Gardena (Los Angeles) California. Her research interests are in the broad area of formal verification, automatic synthesis and repair of systems, and temporal logic. Her current focus is in the area of cyber-physical systems, in particular, automotive control systems modeled as hybrid automata and nonlinear dynamical systems. Previously, Xiaoqing got her PhD in the area of formal verification and validation for hybrid systems under the supervision of Gianfranco Ciardo (who is currently at Iowa State University) at the University of California, Riverside.