Abstract: CMU is beginning a major new research program to develop new programming technology breakthroughs that will enable order-of-magnitude improvements in the quality, development schedule, and cost of embedded and real-time space software systems at NASA. Specific objectives include:

1. Program analysis technology that provides positive assurance of non-local correctness properties of Real-Time Java programs, including the correct use of real-time threads, region-based memory management, and synchronization.
2. Automated, model-checking-based verification of relevant safety and liveness properties of embedded and real-time software systems that are written in high-level languages.
3. Programming language technologies ensuring important low-level correctness properties for real-time systems, including tight bounds on memory and CPU utilization, the lack of memory and concurrency errors, and design conformance.
4. Management-level measures of progress towards assuring the overall dependability of a software system.
5. Application and evaluation of these technologies in a realistic environment, including NASA rovers and other relevant software systems.

Jonathan Aldrich is an Assistant Professor at Carnegie Mellon University. He received his B.S. from the California Institute of Technology, and his M.S. and Ph.D. from the University of Washington. His Ph.D. thesis explored the integration of architectural descriptions into an implementation language, and the usage of a type system to ensure that the architectural structure is consistent with the code. This approach is embodied in ArchJava, which is an extension to Java that seamlessly unifies software architecture with implementation. His dissertation earned him the William Chan Memorial Dissertation Award at the University of Washington.