Cyber-physical systems (CPS) are becoming the key enabler in many engineering domains from traffic management to autonomous vehicles. Concurrency, failures, and their interactions with the physical environment make it challenging to wrestle a high level of confidence from such systems. This project develops a reusable middleware service which enables the creation of verified and hence reliable distributed CPS by pushing the state-of-the-art in two directions: (1) Existing distributed services cannot be practically implemented because of high communication costs incurred in the face of dynamic failures and changes. This project develops a Group Communication Service (GCS) which can be implemented with reasonable resources and which guarantees automatic recovery after failures (stabilization). (2) Existing verification techniques focus on non-distributed CPS, and in general systems with failures, message delays, etc., are unlikely to be amenable to automated analysis. For applications built with the GCS, the project develops a suite of verification tools that exploit stabilization, compositionality, abstraction-refinement, and delay insensitivity of applications. These core research tasks will lead to fundamental advances in design and verification of hybrid and distributed systems.
The outcomes of this project are expected to bolster the dependability of emerging applications in autonomous vehicles and factories, and intelligent surveillance systems, while keeping the development costs acceptable through automation. Through industry collaborations, the research outcomes will be translated into engineering practices. The educational component will provide course and lab modules for graduate, undergraduate, and high-school students with the aim of unifying the physical and the computational viewpoints in the systems curriculum. Through active recruitment and mentoring, women and minority students will be prepared for careers in scientific research.
