Specification based prototyping of control systems

We focus on an approach to simulation and debugging of formal software specifications for control systems called specification-based prototyping. Within the context of specification execution and simulation, specification-based prototyping combines the advantages of traditional formal specifications (e.g., precision and analysis) with the advantages of rapid prototyping (e.g., risk management and early user involvement). The approach lets us refine a formal and executable model of the system requirements specification to a detailed model of the software requirements specification. Throughout this refinement process, the specification is used as an early prototype of the proposed software. By using the specification as the prototype, most of the problems that plague traditional code-based prototyping disappear. First, the formal specification will always be consistent with the behavior of the prototype (excluding real-time response) and the specification is, by definition, updated as the prototype evolves. Second, the common problems associated with evolving the prototype into a production system are largely eliminated. Finally, the dynamic evaluation of the prototype can be augmented with formal analysis. To enable specification-based prototyping, we have developed the NIMBUS requirements engineering environment. NIMBUS, among other things, allows an engineer to dynamically evaluate an RSML^-e (Requirements State Machine Language without events) specification while interacting with (1) user input or text file input scripts, (2) RSML^-e models of the components in the embedding environment, (3) software simulations of the components, or (4) the physical components themselves (hardware-in-the-loop simulation)