Dr. Dimitra Giannakopoulou was one of two invited speakers at the 17th International Workshop on Formal Methods for Industrial-Critical Systems (FMICS) in Paris, France, August 2012. FMICS brings together scientists and engineers to exchange their experiences in the industrial usage of formal methods. Dr. Giannakopoulou was invited as a representative from industry to share both her research contributions to the field of formal methods, and her experience with the application of formal methods within NASA.
Her talk, titled “To Scale or Not to Scale: Experience with Formal Methods and NASA Systems,” discussed her experience with the development and use of formal method techniques in the context of aerospace systems. She first provided an overview of approaches developed in the Robust Software Engineering group over the last decade for scaling exhaustive verification through divide-and-conquer principles. In particular, she presented learning-based frameworks for automatically generating component abstractions. Such abstractions can be used for documentation or more efficient modular reasoning. In the domain of human automation interaction systems, these abstractions can be used by human operators to understand what to expect from their interactions with the system.
The techniques that were presented use a variety of approaches, including model checking, predicate abstraction, and symbolic execution. Despite the progress made in developing and applying sophisticated formal methods frameworks, the issue of scalability still remains the Achilles heel in this domain. Dr. Giannakopoulou discussed scalability and the trade-offs that she has made in her work, as well as her perspective for the future application of formal methods in industry.
The talk was very well received and stirred many interesting discussions among the participants. For more information, see: http://fmt.cs.utwente.nl/conferences/fmics2012/invitedspeakers/.
BACKGROUND: Dr. Dimitra Giannakopoulou is a Research Computer Scientist with the Robust Software Engineering group at the NASA Ames Research Center. Her research focuses on scalable specification and verification techniques for NASA systems. In the context of her project on compositional verification of flight-critical systems, she has been developing novel algorithms and tools for scalable verification and testing of aerospace systems. Examples of target applications include next-generation air-traffic control algorithms and software. She has also been studying the application of formal methods to human automation interaction problems.
NASA PROGRAM FUNDING: Assurance of Flight Critical Systems project, System-wide Safety Assurance Technologies (SSAT) project, Aeronautics Research Mission Directorate (ARMD)
Contact: Dimitra Giannakopoulou