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.