This paper describes the evolution of a software testing effort during a critical period for the flagship Mars Science Laboratory rover project at the Jet Propulsion Laboratory. Formal specification for post-run analysis of log files, using a domain-specific language, LogScope, replaced scripted real-time analysis. Log analysis addresses the key problems of on-the-fly approaches and cleanly separates specification and execution. Mining the test repository suggested the inadequacy of the scripted approach, and encouraged a partly engineer-driven development. LogScope development should hold insights for others facing the tight deadlines and reactionary nature of testing for critical projects. LogScope received a JPL Mariner Award for "improving productivity and quality of the MSL Flight Software" and has been discussed as an approach for other flight missions. We note LogScope features that most contributed to ease of adoption and effectiveness. LogScope is general and can be applied to any software producing logs.

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.

Software verification methods are used only sparingly in industrial software development today. The most successful methods are based on the use of model checking. There are, however, many hurdles to overcome before the use of model checking tools can truly become mainstream. To use a model checker, the user must first define a formal model of the application, and to do so requires specialized knowledge of both the application and of model checking techniques. For larger applications, the effort to manually construct a formal model can take a considerable investment of time and expertise, which can rarely be afforded. Worse, it is hard to secure that a manually constructed model can keep pace with the typical software application, as it evolves from the concept stage to the product stage. We describe a verification method that requires far less specialized knowledge in model construction. It allows us to extract models mechanically from source code. The model construction process now becomes easily repeatable, as the application itself continues to evolve. Once the model is constructed, existing model checking techniques allow us to perform all checks in a mechanical fashion, achieving nearly complete automation. The level of thoroughness that can be achieved with this new type of software testing is significantly greater than for conventional techniques. We report on the application of this method in the verification of the call processing software for a new telephone switch that was developed at Lucent Technologies.

A logic model checker can be an effective tool for debugging software applications. A stumbling block can be that model-checking tools expect the user to supply a formal statement of the correctness requirements to be checked in temporal logic. Expressing non-trivial requirements in logic, however, can be challenging. To address this problem, we developed a graphical tool, called the TimeLine Editor, that simplifies the formalization of certain kinds of requirements. A series of events and required system responses are placed on a timeline. The user converts the timeline specification automatically into a test automaton that can be used directly by a logic model checker or for traditional test-sequence generation. We have used the TimeLine Editor to verify the call processing code for Lucent's PathStar access server against the TelCordia LSSGR [LATA (local access and transport area) Switching Systems Generic Requirements] standards. The TimeLine Editor simplified the task of converting a large body of English prose requirements into formal, yet readable, logic requirements.

Formal verification methods are used only sparingly in software development.The most successful methods to date are based on the use of model checking tools.To use such tools, the user must first define a faithful abstraction of the application (the model), specify how the application interacts with its environment, and then formulate the properties that it should satisfy.Each step in this process can become an obstacle.To complete the verification process successfully often requires specialized knowledge of verification techniques and a considerable investment of time.In this paper we describe a verification method that requires little or no specialized knowledge in model construction.It allows us to extract models mechanically from the source of software applications, securing accuracy.Interface definitions and property specifications have meaningful defaults that can be adjusted when the checking process becomes more refined.All checks can be executed mechanically, even when the application itself continues to evolve.Compared to conventional software testing, the thoroughness of a check of this type is unprecedented.