Modeling techniques that are expressive do not yield as completely to formal analysis. Although abstraction can (and will) be used to construct verifiable views of a system, certain properties will have to be validated by simulation. The simulation environment that is needed has some unique requirements, however. Most notably, it will need to support heterogeneous mixtures of modeling techniques, including hierarchical automata and I/O-based models with discrete-event systems, dataflow, synchronous/reactive, and continuous-time semantics.
We have some prior experience with such simulation environments in the context of the Ptolemy Project. In particular, with DARPA funding, we are currently about halfway through a project entitled Heterogeneous Modeling and Design (HMAD). In that project, we are developing a design methodology, and associated modeling software, for composite, heterogeneous systems. Such systems combine diverse implementation technologies, including microelectromechanical systems (MEMS), microwave circuits, analog circuits, digital circuits, and embedded software. They also combine modeling and design paradigms, including physical modeling using differential equations, continuous-time signal processing, discrete-time signal processing. They are invariably concurrent, involving diverse modules that operate at the same time and interact through continuous signals or discrete messages.
In the proposed project, we will attempt to reuse as much of the software architecture as appropriate to develop a specification and simulation environment for complex control systems. The current incarnation of Ptolemy software, called Ptolemy II, is written in Java and is being developed using modern software engineering techniques including object modeling, design patterns, and a limited amount of software engineering process (limited because of our academic setting). We believe that it provides an excellent platform to build on.