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

Hierarchical Circular Compositional Reasoning

We describe a composition rule for hierarchically composed components that may involve circular reasoning between the components. It is similar to previous work by McMillan, specialized to component level reasoning. In contrast to McMillan's work, our composition rule can be used in provers that only support safety properties (e.g. k-induction model checkers) as long as the system and component contracts consist of state invariants. The composition rule still holds for richer contracts, but the resulting verification conditions then require a general purpose model checker.

Parameterized Abstractions for Reasoning about Algebraic Data Types

Reasoning about algebraic data types is an important problem for a variety of proof tasks. Recently, decision procedures have been proposed for algebraic data types that create suitable abstractions of values in the types. A class of abstractions created from catamorphism functions has been shown to be theoretically applicable to a wide variety of reasoning tasks as well as efficient in practice. However, in previous work, the decidability of catamorphism functions involving parameters in addition to the data type argument has not been studied.

Compositional Verification of a Medical Device System

Complex systems are by necessity hierarchically organized; they are decomposed into subsystems for intellectual control as well as the ability to have the subsystems created by several distinct teams. This decomposition affects both requirements and architecture; the architecture describes the structure and this affects how requirements are ``flowed down'' to each subsystem, and discoveries in the design process may affect the requirements. Demonstrating that a complex system satisfies its requirements when the subsystems are composed is a challenging problem.

Pages