I have been addressing some of these problems by using model based computing. The basic idea is to develop compositional, reusable behavior models for the components of a system. These models are assembled according to the system design to produce a software model for the whole system. This model is used in various ways --- (1) execution to simulate the system for prototyping and productivity analysis, (2) envisionment to produce and verify software for controlling the system, (3) diagnosis of faulty behavior, and (4) generation of explanations of the functioning of the system to produce documentation. Several of these techniques have already been explored for the domain of photocopiers by researchers here.

In order to be able to write such models, I (jointly with Vijay Saraswat
and Radha Jagadeesan) have designed a programming language,
`Hybrid
CC`. This language is declarative, as this is the most convenient way
for systems engineers to express their knowledge. It is a concurrent language,
so component models may be composed by juxtaposition. It can express both
continuous and discrete change, since the systems that we wish to model
have this property. We have given a precise semantics for our language,
and show its expressiveness by various programming examples. We have also
given an algorithm for translating `Hybrid CC` programs into finite
state automata. Recently we have extended `Hybrid CC` to specify
probabilistic information, by first extending `CC` with a probabilistic
combinator, and then extending `Probabilistic CC` across time uniformly,
allowing it to model stochastic processes.

Our preferred technique for language development is to mathematically define a space of processes, and then develop program combinators corresponding to algebraic operations over this space. Using semantics from the design stage itself results in an elegant language, and gives sound reasoning principles about the behavior of programs, which can then be used to verify their correctness.

In a series of papers developing `Hybrid CC`, we give its semantics
and show how these can be used to define a rich space of operators and
programs. The semantics also provides an algorithm to translate a `Hybrid
CC` program into a hybrid automaton, which can be used for verification
and control code generation. Another possibility we are exploring is to
use abstract interpretation for verification --- this can be used to simplify
automata, just like automata homomorphisms do.

Currently I am engaged in the production of several tools to use the
our modeling framework in different ways. Bjorn Carlson and I have implemented
in C an interpreter for `Hybrid CC` programs --- we have implemented
a state-of-the-art interval constraint solver, and a 4th order Runge-Kutta
integrator modified for interval variables and implicitly specified ODE's.
In order to make the system more modular, we have also added a simple object
system to `Hybrid CC`. My summer student, Moses Charikar, and I
have built a tool to produce hybrid automata from `Hybrid CC` programs
--- we will now use it for verification and automatic control code generation.

Our first application was modeling the various components of the paperpath
of a copier. Along with Peter Struss, I developed and implemented in `Hybrid
CC` a compositional model for the paperpath which is simpler than previous
models, yet is applicable in more situations. Currently I am modeling spacecraft
for as part of the effort towards building autonomous systems using model-based
programming. We have built models of the Marsokhod rover, the
Sprint AERCam

robotic camera, a Personal Satellite Assistant and an In-situ Propellant
Production Plant for a Mars mission, among others. `Hybrid
CC` is also being used for modeling systems at Stanford, Toshiba
Corporation, Xerox PARC and other institutions.

In the long term I would like to study the various aspects of building reliable software systems. This would entail looking at specification and programming languages, verification tools, user interfaces and implementation techniques, among other things. I am also interested in looking at techniques from diverse areas of Computer Science and Mathematics for facilitating software creation.