High-Confidence Cyber-Physical Systems

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.

Moreno, Gabriel & de Niz, Dionisio. "An Optimal Real-Time Voltage and Frequency Scaling for Uniform Multiprocessors," 21–30. Proceedings of the IEEE International Conference on Embedded and Real-Time Computing Systems and Applications. Seoul, Korea, August 2012. IEEE Computer Society Press, 2012.

Contact Us

Dionisio de Niz 

Sagar Chaki

Find Us Here

Find us on Youtube  Find us on LinkedIn  Find us on twitter  Find us on Facebook

Share This Page

Share on Facebook  Send to your Twitter page  Save to del.ico.us  Save to LinkedIn  Digg this  Stumble this page.  Add to Technorati favorites  Save this page on your Google Home Page 

For more information

Contact Us

info@sei.cmu.edu

412-268-5800

Help us improve

Visitor feedback helps us continually improve our site.

Please tell us what you
think with this short
(< 5 minute) survey.