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: 
Office Location: 
Kenneth H Keller Hall room 6-254

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

An Approach to Automatic Code Generation for Safety-Critical Systems

Although formal requirements specifications can provide rigorous and unambiguous description of a safety-critical software system, designing and developing production quality code from high-level specifications can be a time-consuming and error-prone process. Automated translation, or code generation, of the specification to production code can alleviate many of the problems associated with design and implementation.

On the Effectiveness of Slicing Hierarchical State Machines: A Case Study

Formal specifications can be hundreds of pages in length — a reflection of the size and complexity of the systems being specified. Lengthy documents are difficult to read, understand, and use. Program slicing was developed to address these issues for programs. In this paper, we apply similar techniques to formal specifications expressed as hierarchical state machines. We present a two tiered approach to slicing (or simpli.cation) of hierarchical state machines.

Reduction and Slicing of Hierarchical State Machines

Formal specification languages are often criticized for being difficult to understand, difficult to use, and unacceptable by software practitioners. Notations based on state machines, such as, Statecharts,