Professional Interests

Research Interests / Other CSCI Interests

Research Interests

My research interests focus on a class of languages called Synchronous Languages that can be used to specify the behavior of process-control or reactive systems. Synchronous languages  have several useful properties for specification:

Because of their relative simplicity and these properties, synchronous languages have a straightforward tech-transfer path, and are being used in several industrial settings.  Notable commercial languages in this class include Simulink, SCADE , Esterel , and MatrixX .

Currently, I am interested in verification and validation of models written in these languages.  In my work at Rockwell-Collins, I have developed translation tools that translate from Simulink and SCADE (Lustre) to a variety of back-end analysis tools, including NuSMV , Prover , SAL , PVS , and ACL2 .  We have used these tools to perform large-scale formal analysis of industrial-sized avionics software models.  We are currently using formal analysis tools for functional verification, model well-formedness properties (e.g., no divide-by-zero), safety analysis, and test-case generation.

I completed my PhD at the University of Minnesota in January, 2005.  As a graduate student, I worked in the Critical Systems Research Group ( CriSys ), where I helped design a synchronous language called Requirements State Machine Language without Events (RSML-e).  My Masters thesis provided the first complete formalization of RSML-e, written in the Z formalism. This formalization has formed the backbone of the RSML-e NIMBUS Simulator and translation tools from RSML-e to model checking and theorem proving tools.  My PhD dissertation re-formalized RSML-e using higher-order abstract syntax and structural operational semantics to create a provably-correct translator from RSML-e to a subset of C. 

Other CSCI Interests

I am interested in general purpose programming languages and software design. I have worked extensively with logic programming languages (?Prolog), functional programming languages (Standard ML) and object-oriented languages (C++) and am familiar with many of the design patterns applicable to compilers and GUI applications. I am interested in improvements in the state of the practice both from new languages, and idioms for working with existing languages. When I have more time, I'll try to expand this section of my web page.

The views and opinions expressed in this page are strictly those of the page author.
The contents of this page have not been reviewed or approved by the University of Minnesota.