Compositional Nonblocking Verification of Discrete Event Systems

Safety-critical control systems are often modeled as discrete event systems that consist of several interacting finite-state machines. This talk explores methods verify the correctness of such system automatically. Specifically, the nonblocking property is considered, which expresses the absence of deadlocks and livelocks in the system. This is a difficult problem for systems with a large number of components due to state-space explosion, and because many standard methods do not apply to the nonblocking property. Nevertheless, recent advances in compositional verification make it possible to verify the nonblocking property for several models of industrial-scale control systems.

Robi Malik received the M.S. and Ph.D. degrees in computer science from the University of Kaiserslautern, Kaiserslautern, Germany, in 1993 and 1997,
respectively. From 1998 to 2002, he worked in a research and development group at Siemens Corporate Research, Munich, Germany, where he was involved in the development and application of modeling and analysis software for discrete-event systems. Since 2003, he is lecturing computer science and software engineering at the Department of Computer Science at the University of Waikato in Hamilton, New Zealand. He is participating in the development of the Supremica software for modeling and analysis of discrete-event systems. His current research interests are in the area of model checking and synthesis of large discrete-event systems and other finite-state machine models.