The CMACS project is focused on far-reaching and transformative research into techniques based on Model Checking and Abstract Interpretation (MCAI) for analyzing the behavior of complex embedded and dynamical systems. Model Checking and Abstract Interpretation have a 30-year record of success at verifying properties of the behavior of discrete systems automatically. The techniques have been fruitfully used, both independently and in combination, to establish properties of systems containing thousands of variables and inputs and several 100,000’s of lines of code (for example, the Airbus 380’s flight control software), and to detect subtle bugs in a variety of hardware and software applications, ranging from microprocessor designs and communication protocols to railway-switching systems and satellite-control software. The purpose of this project is to extend the MCAI paradigm to reasoning about the behavior of models of physical systems that include continuous and stochastic behavior, such as those found in biological and embedded-control areas. Specific research is being undertaken in model discovery / system identification for stochastic and nonlinear hybrid systems; methods for generating sound model abstractions to simplify the reasoning process; and next-generation algorithms for analyzing the behavior of these models. Challenge problems in the area of pancreatic-cancer modeling, atrial-fibrillation detection, distributed automotive control, and aerospace control software are being used as technology drivers and testbeds for the results obtained in the course of the project.

Model Checking

A model checker can determine whether or not a system satisfies (is a model of) a property describing desired behavior of the system. Properties are typically stated in temporal logic, for example G(req => F ack) indicates that it is invariably the case (G=globally) that a request eventually (F=in the future) triggers an acknowledgment. Two especially noteworthy aspects of Model Checking are: (1) when the system model is finite-state, Model Checking can be performed algorithmically; and (2) when the system is found to violate the property, a counterexample in the form of a system execution is generated that can be used to debug the system model or property.

Abstract Interpretation

As the name suggests, Abstract Interpretation can be viewed as defining nonstandard/ abstract executions of a program that reveal information about the program’s semantics (for example, control structure, flow of information) without performing all of the underlying concrete calculations. Its main application is static analysis, the automatic extraction of information about the possible executions of a computer system for the purpose of compiler optimization and verification of safety and security properties.

MCAI 2.0

A key driver for the project is our belief that the seemingly different Challenge Problems share mathematical similarities that will permit common MCAI technology to be applied to solving them. Coping with continuous, stochastic and infinite-state behavior will require fundamental new research leading to MCAI 2.0, a new suite of methodologies and tools—including singular perturbation, hybridization, differential invariants and statistical techniques—for compositionally approximating, abstracting, and analyzing properties of complex systems.

The development of MCAI 2.0 thus requires ground-breaking research in a number of cross-cutting areas, including Model Discovery, Novel Abstractions, Next-Generation Verification and Analysis, and Challenge Problems as Technology Drivers. See also the Strategic Plan diagram.