The Logical Systems Laboratory at Carnegie Mellon University hosted an NSF-sponsored workshop on Cyber-Physical System Verification & Validation: Industrial Challenges & Foundations December 11-12, 2014. This productive workshop combined talks on challenges and solutions for analyzing industrial cyber-physical systems with lively panel discussions. The mixed audience included a wide range of representatives from academia and industry, from both the aerospace and automotive industries. Dr. Kristin Yvonne Rozier had the honor of giving the opening talk on “Integration of Formal Methods into Design and Implementation of Aerospace Systems,” issuing challenges compiled from years of industrial experience.
ABSTRACT: The value of formal methods in aerospace system design and verification has been demonstrated increasingly frequently, leading to more widespread acknowledgment of the essentialness of incorporating these methods into any safety-critical project. However, the success stories have mainly demonstrated the value of the results of formal methods analysis, advancing formal techniques in terms of scalability, efficiency, and adaptability to the range of complex problems in the aerospace domain. While this has gone a long way to winning over the perception of formal methods as a valuable and integral tool, it has not addressed some of the most significant bottlenecks in the process and the original barriers to adaptation. These challenges include creating a formal model and extracting formal specifications from a development process that might never before have created them. This talk will briefly survey the successes and highlight the remaining barriers to adaptation of formal methods in aerospace. Unless we address these challenges in the near future, the progress of formal methods in aerospace may be stalled.