Registered user since Mon 31 Oct 2016
Dr. Michael Whalen is a Principal Applied Scientist at Amazon Web Services and the former Director of the University of Minnesota Software Engineering Center. He has more than 25 years of experience in software development and analysis, including 15 years of experience in Model-Based Development & safety-critical systems. Dr. Whalen has developed simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. He has led successful large-scale formal verification projects on industrial avionics systems, including displays (Rockwell-Collins ADGS-2100 Window Manager, deployed on the Boeing 787), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program). Dr. Whalen was the lead developer of the Rockwell-Collins Gryphon tool suite, which was used for compilation, test-case generation, and formal analysis of Simulink/Stateflow models. He is currently working on the AGREE tool suite for architectural analysis and testing in AADL, which was recently used to verify correct system behavior in the Boeing Little Bird autonomous helicopter as part of the DARPA HACMS project.
Dr. Whalen is a frequent speaker and author on the use of formal methods and automated testing, with 44 invited presentations, 16 journal publications, one book chapter, 72 conference and workshop papers, and 12 contractor and technical reports published. He has two ICSE and one DASC distinguished papers related to testing, as well as three distinguished papers related to novel uses of model checking. His PhD dissertation involved using higher-order abstract syntax as a basis for a provably-correct code generation tool from the RSML-e specification language into a subset of C. He is currently working on formal verification at “cloud scale”, looking at how to create proof engines that can cost-effectively scale to larger and more complex problems than are handled by current tools. He is also involved with outreach, helping developers and business customers apply verification tools to improve their team’s quality, velocity, and innovation.
Contributions