Contact:Brink van der Merwe
- 8084232
Location: K303, Knowledge Centre, Engineering Complex
ABSTRACT
Recent advances in symbolic verification tools make it possible to
rigorously analyze, and in many cases prove, whether software meets its requirements. These tools have the potential to substantially improve software verification and validation - but only if we have good requirements. Combining symbolic verification with model-based development allows a powerful new approach for early validation of requirements.
This talk discusses experiences at Rockwell Collins and the University of Minnesota in formalizing natural language “shall” statements and applying model checking tools on a variety of industrial avionics models, including displays, flight guidance mode logic, and sensor fusion and voting.
BIO
Dr. Michael Whalen is the Director of the University of Minnesota Software Engineering Center. His interests include formal analysis, language translation, testing, and requirements engineering. He has developed analysis tools for several Model-Based Development languages and has published more than 60 papers on these topics. He has led successful formal verification projects on large industrial models, and has recently been researching tools and techniques for scalable compositional analysis, testing and system image generation from architectural models for quadcopters and autonomous helicopters.
