University of Minnesota
Software Engineering Center
/

You are here

Michael Whalen

Photo of Michael Whalen
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

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts

Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of reactive systems from propositional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of AE-formulas. In spirit of IC3 / PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions.

Architecture Modeling and Analysis for Safety Engineering

Architecture description languages such as AADL allow systems engineers to specify the structure of system architectures and perform several analyses over them, including schedulability, resource analysis, and information flow. In addition, they permit system-level requirements to be specified and analyzed early in the development process of airborne and ground-based systems. These tools can also be used to perform safety analysis based on the system architecture and initial functional decomposition.

Challenges in Testing Next Generation CPS Systems

Testing cyber-physical systems presents a unique set of testing challenges: heterogeneity, timing, and, especially, observability. In particular, some of the mechanisms that are designed to make embedded software robust are the same mechanisms that present challenges for automated testing techniques: e.g., rate limiting, fault masking, and debounce logic, which can lead to long lags between problematic inputs and their manifestation in system outputs. In addition, much of the control behavior of CPS is mathematically intensive more than "branchy".

Pages