Laboratory for Reliable Software (LaRS)
Spacecraft depend on reliable software. Without properly designed control software, a modern spacecraft cannot communicate, navigate or perform science experiments. Reliable software, like reliable hardware, is critical to the success of a mission. But, software is sometimes hard to get right, and it tends to get harder for each new mission.
The size of the control software for spacecraft increases every year, as larger memories and faster processors become available. But not just the amount of software that we rely on is increasing rapidly; the complexity of that software is also increasing. The use of multi-threaded code, for instance, creates opportunities for software defects that are notoriously hard to detect with existing testing methods (e.g., race conditions and deadlocks). While it becomes increasingly important to secure the reliability of mission critical software, it becomes increasingly difficult to thoroughly test that same software.
JPL’s Laboratory for Reliable Software, LaRS, was created in the Spring of 2003 to address this challenge. The Lab’s mission is to achieve long term improvements in the reliability of JPL’s mission critical software systems. To do so, the members of the lab pursue a strong research program that targets the application of formal verification techniques to flight software. Part of the charter of the Lab is to identify weaknesses in the currently used software development processes and to pro-actively identify or develop effective remedies. LaRS’s research is focused on improved software defect prevention methods, defect detection methods, and software fault containment methods.
The scope of attention includes the entire software life-cycle, beginning with requirements capture and analysis, high-level and low-level design, coding, testing, and deployment of software. The topics of interest include:
- requirements capture, analysis, and tracking
- design verification
- static source code analysis
- logic model checking
- automata based testing
- runtime monitoring
- software quality and reliability metrics
- auto coding techniques
- verification of AI-based planners
- verification of fault protection code
- fault tolerance, fault containment, survivability
Focus on Tools and Automation
LaRS targets a tool-based approach to software development, with the explicit objective to move away from the currently used human-driven processses for defect detection and prevention. Software requirements, for instance, are currently often specified in informal English prose with loosely defined syntax (e.g., stylized use of the terms must, shall and will). Instead, a notable fraction of software requirements can be stated in machine-readable form, in a notation that has a more precisely defined meaning, such that tools can be used to analyze the requirements for consistency and completeness, and may even be able to mechanically generate test cases from them.
Similarly, instead of relying on peer review and code walkthrough processes in the early design and coding phases of flight software development, LaRS aims to develop tools that assist the designer with model-based design reviews based on the use of design and formal verification tools, and thorough static source code analysis techniques.
Working with Projects and Missions
LaRS works in collaboration with JPL missions and projects, sometimes volunteering to investigative work, sometimes responding to a request for help. The Lab can take the initiative to evaluate externally available tools and technologies, to assess the level of readiness for use on projects within JPL, and make focused recommendations to JPL projects. In 2004, for instance, LaRS performed an in-depth evaluation of both commercial and academic static source code analysis tools, and determined which of these tools were most suitable for use within JPL. LaRS also made the selected tools available to projects within JPL, under their own licenses.
Foundational Research
When the members of LaRS identify a critical problem in the software development process that has no readily available solution, they can take the initiative to perform targeted research to develop a longer term solution to that problem. An example of such a problem that LaRS is investigating is the verification of multi-threaded software systems. LaRS is working on a new methodology that employs a state of the art model checker (Spin) that can be linked to implementation level code to perform extra-ordinarily thorough types of testing. The Spin model checker, one of the most widely used formal verification systems in the world today, was developed by one of the founding members of LaRS.
LaRS Profile
The members of LaRS organizationaly belong to System and Software Division at JPL. LaRS is currently actively recruiting to build a core group of approximately six JPL researchers with strong background in formal software verification techniques. A larger group of JPL employees is currently associated with LaRS, and collaborates with the group on selected projects. Outside of JPL, LaRS also forms collaborations with other NASA centers, as well as with the leading universities and industrial research labs. The members of LaRS themselves are recruited from among the leaders in software reliability research worldwide.
Website: http://eis.jpl.nasa.gov/lars
Contact:
Gerard Holzmann
Jet Propulsion Laboratory
MS 301-230
4800 Oak Grove Drive
Pasadena, California 91109-8099
E-mail: Firstname.Lastname@jpl.nasa.gov
Tel: (+1 818) 393-5937
Fax: (+ 818) 393-0028
