University of Minnesota
Software Engineering Center
/

You are here

Michael Whalen

Photo of Michael Whalen
Director of the Software Engineering Center
Assistant Professor
Phone Number: 
612-624-5130
Office Location: 
Kenneth H Keller Hall room 6-254
Biography: 

Dr. Michael Whalen is the Program Director at the University of Minnesota Software Engineering Center. He has 15 years experience in software development and analysis, including 10 years 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 formal verification projects on large industrial avionics models, including displays (Rockwell-Collins ADGS-2100 Window Manager), 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 can be used for compilation, test-case generation, and formal analysis of Simulink/Stateflow models. This tool suite has been used both for academic research and industrial verification projects.

Dr. Whalen is a frequent speaker and author on the use of formal methods, with 10 invited presentations, five journal publications, one book chapter, 19 conference papers, and 7 contractor and technical reports published. 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. His interests include novel uses of model checking, test generation, theorem proving, and random search simulation tools to reduce the cost and manual effort required for systems and software validation for critical systems.

Recent Publications

The Risks of Coverage-Directed Test Case Generation

A number of structural coverage criteria have been proposed to measure the adequacy of testing efforts. In the avionics and other critical systems domains, test suites satisfying structural coverage criteria are mandated by standards. With the advent of powerful automated test generation tools, it is tempting to simply generate test inputs to satisfy these structural coverage criteria. However, while techniques to produce coverage-providing tests are well established, the effectiveness of such approaches in terms of fault detection ability has not been adequately studied.

Automated Oracle Data Selection Support

The choice of test oracle—the artifact that determines whether an application under test executes correctly—can significantly impact the effectiveness of the testing process. However, despite the prevalence of tools that support test input selection, little work exists for supporting oracle creation. We propose a method of supporting test oracle creation that automatically selects the oracle data—the set of variables monitored during testing—for expected value test oracles. This approach is based on the use of

Towards Realizability Checking of Contracts using Theories

Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate architectural descriptions and compositional reasoning rules, these techniques can be used to prove important safety properties about the architecture prior to system construction.

Pages