Cyber-Physical Systems are a natural consequence of an increasingly connected physical world.
Cyber-physical systems (CPS) are "engineered systems that are built from, and depend upon, the seamless integration of computational algorithms and physical components" (NSF). Our objective is to enable efficient development of high-confidence distributed CPSs whose nodes operate in a provably correct manner in terms of functionality and timing (synchronicity between physical and software components), leading to predictable and reliable behavior of the entire system. To this end, we develop scalable algorithms for functional analysis of real-time software, techniques for controlling and analyzing the effects of multicore memory access on CPS real-time behavior, and techniques for assuring coordination strategies. We also target both deterministic and stochastic CPSs. Accordingly, our research includes a number of mutually reinforcing threads.
Timing Verification to guarantee that tasks in real-time systems complete within their deadlines. For instance, the airbag of a car must completely inflate within 20 ms;otherwise, the driver can hit the steering wheel with fatal consequences. We are developing schedulability techniques for multicore platforms, where new challenges of shared resources, such as memory, invalidate previous assumptions in single core. We are also developing scheduling techniques for mixed-criticality systems. In addition, we want to incorporate elements of the physical processes to improve qualities of the system such as resilience and performance.
Functional Verification to ensure that software behaves as required. We are developing new model checking algorithms for periodic real-time software to ensure logical correctness properties, such as absence of race conditions, deadlocks, and other concurrency errors that may lead to unsafe or undesired behavior. We also use model checking and code generation to produce high-assurance distributed software.
Probabilistic Verification to maximize the likelihood that a CPS will meet its desired goals. We are exploring probabilistic analysis techniques to estimate, with high accuracy, the chances of a desired goal being achieved (or an undesired outcome being avoided). In particular, we are investigating two analysis techniques: (a) numerical approaches based on probabilistic model checking of Markov chains and Markov decision processes, and (b) techniques based on Monte Carlo simulation such as statistical model checking and importance sampling.
The SEI helps organizations to