University of Minnesota
Software Engineering Center
/

You are here

Michael Whalen

Photo of Michael Whalen
Director of the Software Engineering Center
Director of Graduate Studies
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

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

A flexible and non-intrusive approach for computing complex structural coverage metrics

Software analysis tools and techniques often leverage structural code coverage information to reason about the dynamic behavior of software. Existing techniques instrument the code with the required structural obligations and then monitor the execution of the compiled code to report coverage. Instrumentation based approaches often incur considerable runtime overhead for complex structural coverage metrics such as Modified Condition/Decision (\mcdc). Code instrumentation, in general, has to be approached with great care to ensure it does not modify the behavior of the original code.

Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites

Structural coverage metrics have traditionally categorized code as either covered or uncovered. Recent work presents a stronger notion of coverage, checked coverage, which counts only statements whose execution contributes to an outcome checked by an oracle. While this notion of coverage addresses the adequacy of the oracle, for Model-Based Development of safety critical systems, it is still not enough; we are also interested in how much of the oracle is covered, and whether the values of program variables are masked when the oracle is evaluated.

Pages