Requirements Capture with RCAT

NASA spends millions designing and building spacecraft for its missions. The dependence on software is growing as spacecraft become more complex. With the increasing dependence on software comes the risk that bugs can lead to the loss of a mission. At NASApsilas Jet Propulsion Laboratory new tools are being developed to address this problem. Logic model checking and runtime verification can increase the confidence in a design or an implementation. A barrier to the application of such property-based checks is the difficulty in mastering the requirements notations that are currently available. For these techniques to be easily usable, a simple but expressive requirement specification method is essential. This paper describes a requirements capture notation and supporting tool that graphically captures formal requirements and converts them into automata that can be used in model checking and for runtime verification.