The objective of the High-Confidence Cyber-Physical Systems Project is to enable efficient development of autonomous CPSs whose distributed elements operate in a provably correct and timely manner and consequently whose collective behavior can be predicted and relied on. This entails demonstrating scalable algorithms for functional analysis of real-time software, techniques for controlling effects of multicore memory access on CPS real-time behavior, and techniques for assuring distributed autonomous coordination. Accordingly, our current research includes a number of mutually reinforcing threads.

1. Schedulability analysis 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 extending schedulability techniques to work for multicore platforms where new challenges of shared resources, such as memory, invalidate previous assumptions in single core. In addition, we want to incorporate elements of the physical processes to improve qualities of the system such as resilience and performance.
2. Static analysis of 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 are currently exploring the use of software model checking to verify periodic programs (i.e., consist of tasks that execute periodically with rate-monotonic scheduling). Our goal is to make the verification of such systems more precise and scalable. In addition, we want to model the environment in a way that is more faithful to physical laws, for example, via differential equations.
3. Assuring quality of distributed coordination schemes to maximize our confidence that an autonomous 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, two such analysis techniques are (a) numerical approaches based on analyzing Markov chains and Markov decision processes and (b) techniques based on Monte Carlo simulation such as statistical model checking.
   

References

Andersson, Bjorn & de Niz, Dionisio. "Analyzing Global-EDF for Multiprocessor Scheduling of Parallel Tasks." Proceedings of the 16th International Conference on Principles of Distributed Systems. Rome, Italy, December 2012.

Chaki, Sagar; Gurfinkel, Arie; & Strichman, Ofer. "Time-Bounded Analysis of Real-Time Systems," 72–80. Proceedings of the International Conference on Formal Methods in Computer-Aided Design. Austin, TX, Oct.–Nov. 2011. ACM Press, 2011.

de Niz, Dionisio; Wrage, Lutz; Storer, Nathaniel; Rowe, Anthony; & Rajkumar, Ragunathan. "On Resource Overbooking in an Unmanned Aerial Vehicle," 97–106.  Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems. Beijing, China, April 2012. ACM Press, 2012.