Specification-based Prototyping in NIMBUS
Assurance that a formal specification (system specification or
software specification) possesses desired properties can be achieved
through (1) manual inspections, (2) formal verification of the
desired properties, or (3) simulation and testing of the
specification. To achieve the high level of confidence in the
correctness required in a safety-critical system, all three
approaches must be used in concert. The Critical Systems group has
developed an environment, called NIMBUS, that provides support for
all these activities (Figure 1
). The three V&V techniques fill complementary roles
within the validation and verification process. Manual
inspections and visualization provide the specification team,
customers, systems engineers, and regulatory representatives the
means to informally verify that the behavior described formally in
the specification matches the desired “real world” behavior of
the system. Formal analysis is helpful to determine if the
specification possesses desirable properties, for instance, if the
specification is complete and consistent, and whether unsafe states
are reachable. Simulation and testing helps the analyst to
evaluate and address poorly understood aspects of a design, improves
communication between the different parties involved in development,
allows empirical evaluation of design alternatives, and is one of
the more feasible ways of validating a system’s behavior.
Figure 1: An overview of the NIMBUS architecture.
CriSys has developed an approach to simulation and validation of
formal specifications for process-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., preciseness and analyzability) with the
advantages of rapid prototyping (e.g., risk management and early
end-user involvement). The approach lets an engineer refine a formal
executable model of the system requirements to a detailed model of
the software requirements. 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 risk of evolving the prototype
into a poorly designed production system is largely eliminated.
Finally, the dynamic evaluation of the prototype can be augmented
with formal analysis.
To enable specification-based prototyping, NIMBUS, among other
things, allows an engineer to dynamically evaluate an RSML-e
(Requirements State Machine Language, without events—a fully
formal synchronous data-flow modeling language developed at the
University of Minnesota) specification while interacting with (1)
user input or text file input scripts, (2) RSML-e
models of the components in the environment, (3) software
simulations of the components, or (4) the physical components
themselves.
Figure 2: The NIMBUS Environment’s execution
capabilities.
The execution
capabilities of the NIMBUS environment are based on the ideas that
(1) the engineers would like to have an executable specification of
the system early in the project and (2) as the specification is
refined, it is desirable to integrate it with more detailed models
of the embedding environment. Therefore, in the initial stages
of the project, an engineer may want the executions to take their
input from simple models, for example, text files or user input.
As the specification is refined, the engineer can add more detailed
models of the sensors and actuators, for example, additional
RSML-e specifications or software simulations.
In order to have a closed loop simulation, a model of the process
can be added between the sensor and actuator models. Finally,
when the specification has been refined to the point of defining the
hardware interfaces, the analyst can execute it directly with the
hardware. This hardware-in-the-loop simulation closes the gap
between the prototype and the actual hardware. These ideas are
illustrated in Figure 2
.
The CriSys group
has successfully evaluated the capabilities on various case studies
from the avionics, transportation, and mobile robotics domains.
Download Nimbus and some examples.
|
