University of Minnesota
Software Engineering Center

You are here

Nimbus: A Tool for Specification Centered Development

Date of Publication: 
September 2003
Associated Research Groups: 
Publication Files: 
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. We have developed an specification language, called \rsml, and an environment, called \nimbus, which provides support for all these activities (Figure \ref{fig:nimbus-framework}). The three V\&V techniques fill complementary roles within the validation and verification process. Manual inspections and visualization provide the specification team, customers, and regulatory representatives the means to informally verify that the behavior described formally matches the desired ``real world'' behavior of the system. Formal analysis is helpful to determine if the specification possesses desirable properties. 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.
Proceedings of the 11th IEEE International Requirements Engineering Conference, Monterey Bay, California, September, 2003.
@InProceedings{Heimdahl03:Nimbus, author = {Mats P.E. Heimdahl and Michael W. Whalen and Jeffrey M. Thompson}, title = {Nimbus: A Tool for Specification Centered Development}, booktitle = {Proceedings of the 11th IEEE International Requirements Engineering Conference}, year = {2003}, month = {September} }