Control Seminar

Compositional Nonblocking Verification of Discrete Event Systems

Robi Malik

Senior Lecturer
University of Waikato
Tuesday, June 12, 2018
11:00am - 12:00pm
1008 EECS

Add to Google Calendar

About the Event

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.

Additional Information

Contact: Judi Jones

Phone: 763-8557


Sponsor(s): ECE

Faculty Sponsor: Stephane Lafortune

Open to: Public