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. In addition, we develop, analyze, and validate portable architecture and middleware to support user-directed groups of autonomous sensors and systems. 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.
Collaborative Autonomy to optimize scalability, performance, and extensibility for autonomous systems by creating a portable, open-sourced, decentralized operating environment. We integrate this environment into unmanned autonomous systems (UAS) platforms, smartphones, tablets, and other devices and design algorithms and tools to perform mission-oriented tasks. We also design user interfaces to help single human operators control and understand a swarm of UAS, devices, and sensors.
Self-Adaptation to address the challenge of having cyber-physical systems that can quickly adapt to a variety of situations including environment changes, and malfunctions. A self-adaptive system is a system capable of changing its behavior and structure to adapt to changes in itself and its operating environment without human intervention. We are developing architecture-based self-adaptation approaches that take into account the latency of the available adaptation strategies when deciding how to adapt. Furthermore, our techniques leverage short term predictions of the environment evolution to enable proactive adaptation.
The SEI helps organizations to