Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology

Professor Rance Cleaveland (CS/ISR) is the principal investigator and Professor Steve Marcus (ECE/ISR) is a co-PI for the University of Maryland’s portion of a major new National Science Foundation collaborative research grant, “Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology.” The five-year, $10 million project is part of NSF’s “Expeditions in Computing” initiative. Maryland’s part of the project is worth $1.8 million. Along with Marcus, Tongtong Wu of the University of Maryland’s School of Public Health is also a co-PI. The consortium will develop new computational tools to help scientists and engineers analyze and understand the behavior of the complex models they develop for application domains ranging from systems biology to embedded control. Building on the success of model checking and abstract interpretation (MCAI), two well-established methods for automatically verifying properties of digital circuit designs and embedded software, this research project will extend the MCAI paradigm to systems with complex continuous dynamics and probabilistic behaviors. The research will include: understanding the precursors and course of pancreatic cancer; predicting the onset of atrial fibrillation; and obtaining deep design-time insights into the behavior of automotive and aerospace control systems. Ultimately, the project is expected to provide vital tools that will enable health care researchers to discover better treatments for disease and will allow engineers to build safer aircraft and other complex systems.