Volume 10, Number 5 • September/October 2002 • Advanced Technologies

Making Software More Reliable

Research is currently being conducted at NASA Ames in Moffett Field, CA on the ability of software to find its own errors.

The validation and verification (V&V) of software is being studied throughout the software industry, but the goal of this particular project is to demonstrate scalable, or size-adaptable, analytic verification technology (making sure the coding is right) on a major subsystem for aerospace. The approach is to advance the capabilities of model-checking technology to support verification of software and to evaluate the technology on realistic examples obtained from collaborations with aerospace companies. Researchers have presented the results of several case studies in applying model checking to software that was used to guide the research—notably the application of model checking to a real-time embedded aerospace operating system (DEOS) to discover a subtle error not uncovered during testing. From several years of research, the results have been a set of synergistic
verification algorithms, or mini programs, that enable the analysis of large verification problems.

The cost of software aspects of flight certification for avionics systems has grown significantly in recent years because of the increased complexity of software in avionics systems. This software provides advanced control, communication and safety features at a reduced cost and weight. However, verification and certification of software for high levels of assurance is extremely expensive due to the manual effort needed to support the extensive testing required by the Federal Aviation Administration (FAA).

The difficulty of verification and certification will continue to increase due to an industry trend toward Integrated Modular Avionics (IMA), which aims to further reduce costs. IMA allows multiple applications of varying criticality levels to execute on a shared computing resource. Part of the cost-savings strategy of IMA is that software applications will be individually certified, allowing them to be mixed-and-matched with avionics platforms. Currently, this is not supported by the FAA certification process, which takes the approach of certifying each platform configuration separately. This new approach researched by NASA Ames is promising because it is well known that individual testing of an IMA is inadequate to assure that arbitrary combinations of applications will operate together safely, as they are not generally tested together.

Reducing the manual effort required to support certification and, at the same time, increasing the levels of assurance, will require significant advances in software verification and certification technology. There is a class of technologies called analytical verification tools that has the potential to address these issues. These techniques involve the analysis of mathematical models of software systems, which are based on the execution semantics of the software. The analytical verification tools include model checking, static analysis and abstract interpretation. To enable these tools to support verification of real avionics systems, the applicability and scalability of these techniques must be improved. In addition, methods for applying the tools and quantifying benefits of using them to support verification must be developed to integrate the new technology into the certification process. The tools and techniques also must be integrated with standard engineering methods and processes to be cost-effective.

The general technical thrust of research develops technology that allows the use of model checking to support the analysis of critical avionics software systems. Specifically, the focus develops advanced model-checking algorithms to support object-oriented programming languages. This approach addresses the applicability and scalability of model checking, while providing a tighter integration with engineering by directly supporting programming language models. To provide further scalability, extending automated program abstraction technology to allow model checking of complex software systems has worked well. Automated techniques have also been developed for verification test driver generation, which addresses one of the major costs of applying the tools in practice.

This research approach has developed prototype tools to evaluate technology on real systems and provide potential near-term benefits. The main tool that has been developed is the Java PathFinder model checker. As part of the evaluation process, Honeywell Technology Center has been given the ability to analyze several versions of their DEOS real-time operating system, which has increased confidence in the implementation of critical aspects of this system.

Due to the size of real-world software systems, the majority of work to date has focused on defect detection rather than producing guarantees that behavioral properties of the software are satisfied. Exhaustive model checking of all system behavior is not possible due to memory limitations. It is, however, possible to give guarantees of the absence of certain errors if a partial analysis of the system is done. More precisely, by analyzing a system with an environment that cannot perform all possible legalactions at any time, then it still may well be possible to show the system behaves correctly. Therefore, by guaranteeing that during execution the environment only executes actions that have been analyzed, then the system will behave correctly. It is easy to use runtime monitoring to check that the system execution stays within the analyzed bounds. It is even possible to go a step further by initiating a recovery unit whenever the bounds are exceeded. Of course, the bounds need not just be on environment behavior, but might be predicated on the behaviors analyzed during model checking, which may include restrictions of system behavior not influenced by the environment.

In the next phase of the project, techniques will be developed to capture restrictions on system behavior under which absence of errors can be guaranteed in such a way that one can use runtime monitoring and recovery to maintain correct system behavior. In preliminary work, it has been shown that one can use certain filters on environmental behavior to show absence of certain errors. These filters can then be used within a runtime monitor that can check such properties during system execution.

A long-term goal for this research is to develop techniques by which the model checker can “learn” the structure of the system, and therefore the shape of the graph of reachable states, which will ultimately optimize the analysis of the system. Q

For more information, contact David Lackner at the NASA Ames Research Center Commercial Technology Office, Mail Stop 202A-3, Moffett Field, CA 94035-1000, phone: 650/604-5761, fax: 650/604-1592, dlackner@mail.arc.nasa.gov, Web site: http://technology.arc.nasa.gov. Please mention you read about it in Innovation.

NASA Official: Jonathan Root • Web Design: Printing & Design Office, NASA Headquarters • Credits