Professional Interests

Research Interests / Other CSCI 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:

Natural mapping between the language and real-world problems
Easy readability
Relatively simple formal semantics
Executability
Analyzability

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.