The goal of functional verification is to ensure that the behavior of CPS software respects its specification when executing in a given environment. We are targeting both deterministic and stochastic systems. The specification expresses a safety condition, (e.g., no deadlocks, no violations of user-specified assertions) that must be satisfied in all possible executions of the software (for deterministic systems) or with some required minimum likelihood (for stochastic systems). The environment captures details of software (e.g., number of threads and their priorities), the operating system (e.g., scheduling policy), and the nature of communication (e.g., shared memory, message passing). We have two main research directions in functional verification:
Our solutions are based on automated and exhaustive techniques (such as model checking and probabilistic model checking). We publish our results in peer-reviewed venues, and implement our algorithms in prototype tools, which are validated on examples guided by real-life systems and scenarios.
Further details are available on individual project web pages.