University of Minnesota
Software Engineering Center

You are here

Mats Heimdahl

Photo of Mats Heimdahl
Computer Science and Engineering Department Head
Phone Number: 
Office Location: 
Kenneth H Keller Hall room 6-201

M.S. Computer Science and Engineering from the Royal Institute of Technology, Sweden, 1988.

Ph.D. Computer Science, University of California at Irvine, 1994.


Professor Mats Heimdahl specializes in software engineering and safety critical systems. He is the director of the University of Minnesota Software Engineering Center (UMSEC).

Heimdahl is the recipient of the National Science Foundation's CAREER award, a McKnight Land-Grant Professorship and the McKnight Presidential Fellow award at the University of Minnesota, and the University of Minnesota Award for Outstanding Contributions to Post-Baccalaureate, Graduate, and Professional Education.


Software is increasingly involved in our lives; software controls physical systems ranging from microwave ovens and watches to nuclear power plants, aircraft, and cars. Computer-related failures can, in many of these applications, have catastrophic effects.

My research group, the Critical Systems Research Group (CriSys), is conducting research in software engineering and is investigating methods and tools to help us develop software with predictable behavior free from defects.

Research in this area spans all aspects of system development ranging from concept formation and requirements specification, through design and implementation, to testing and maintenance. In particular, we are currently investigating model-based software development for critical systems.

Specifically, we are focusing on how to use various static verification techniques to assure that software requirements models possess desirable properties, how to correctly generate production code from software requirements models, how to validate models, and how to effectively use the models in the testing process.


Software engineering and safety critical systems.

Recent Publications

Mode Confusion Analysis of a Flight Guidance System Using Formal Methods

Advancements in digital avionics systems have accounted for much of the improvement in air safety seen over the last few decades. At the same time, the growing complexity of these systems places greater demands on the flight crew and increases the risk of mode confusion, a phenomenon in which pilots become confused about the status of the system and interact with it incorrectly. To fly commercial flights today, pilots must master several complex, dynamically interacting systems, often operating at different levels of automation.

Nimbus: A Tool for Specification Centered Development

Assurance that a formal specification (system specification or software specification) possesses desired properties can be achieved through (1) manual inspections, (2) formal verification of the desired properties, or (3) simulation and testing of the specification. To achieve the high level of confidence in the correctness required in a safety-critical system, all three approaches must be used in concert. We have developed an specification language, called \rsml, and an environment, called \nimbus, which provides support for all these activities

Model Checking RSML-e Requirements

Model checking is a promising technique for automated verification or refutation of software systems. Nevertheless, it has not been used widely in practice mainly due to the lack of the supporting tools that incorporate the model checking activity into the development process. As a part of our overall method supporting specification centered system development, we have implemented a translator between a formal specification language RSML-e and a symbolic model checker NuSMV. Our translation and abstraction approach aims at usability in