Home ยป Directory

Michael Whalen

Michael Whalen
Visiting Researcher
Phone Number: 
612-625-4543
Biography: 

Michael W. Whalen is interested in several aspects of software engineering, including requirements gathering processes and notations, formal analysis of requirements models and code, and in formal description and analysis of transformational systems such as compilers. He is a Ph.D. Candidate in Computer Science from the University of Minnesota. His dissertation work describes techniques for reasoning about code transformations in order to prove the correctness of compilers and code generators.

Mr. Whalen is an employee of Rockwell-Collins and acts as a liason between Rockwell and the University of Minnesota on a large research project sponsored by NASA Langely and Rockwell Collins investigating advanced methods and tools for the development of flight critical software. Mr. Whalen has 10 years of software development experience, and has helped develop several large software systems including a transaction monitoring system, a software requirements engineering tool, and several translators and compilers.

Recent Publications

Extending Lustre with Timeout Automata

Date of Publication: 
April 2007
Authors: 
Jimin Gao
Authors: 
Michael Whalen
Authors: 
Eric Van Wyk
Abstract: 
This paper describes an extension to Lustre to support the analysis of globally asynchronous, locally synchronous (GALS) architectures. This extension consists of constructs for directly specifying the timeout automata used to describe asynchronous communication between processes represented by Lustre nodes. It is implemented using an extensible language framework based on attribute grammars that allows such extensions to be modularly defined so that they may be more easily composed with other language extensions.

A Proposal for Model-Based Safety Analysis

Date of Publication: 
October 2005
Authors: 
Anjali Joshi
Authors: 
Steven Miller
Authors: 
Michael Whalen
Authors: 
Mats Heimdahl
Abstract: 
System safety analysis techniques are well es-tablished and are used extensively during the design of safety-critical systems. Despite this, most of the techniques are highly subjective and dependent on the skill of the practitioner. Since these analyses are usually based on an informal system model, it is unlikely that they will be complete, consistent, and error free. In fact, the lack of precise models of the system architecture and its failure modes often forces the safety analysts to devote much of their effort to finding undocumented details of the sys-tem behavior and embedding this information in the safety artifacts such as the fault trees.

Nimbus: A Tool for Specification Centered Development

Date of Publication: 
September 2003
Authors: 
Mats Heimdahl
Authors: 
Michael Whalen
Authors: 
Jeffrey Thompson
Abstract: 
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 (Figure \ref{fig:nimbus-framework}). The three V\&V techniques fill complementary roles within the validation and verification process.
more