Software assurance by bounded exhaustive testing

Bounded exhaustive testing (BET) is a verification technique in which software is automatically tested for all valid inputs up to specified size bounds. A particularly interesting case of BET arises in the context of systems that take structurally complex inputs. Early research suggests that the BET approach can reveal faults in small systems with inputs of low structural complexity, but its potential utility for larger systems with more complex input structures remains unclear. We set out to test its utility on one such system. We used Alloy and TestEra to generate inputs to test the Galileo dynamic fault tree analysis tool, for which we already had both a formal specification of the input space and a test oracle. An initial attempt to generate inputs using a straightforward translation of our specification to Alloy did not work well. The generator failed to generate inputs to meaningful bounds. We developed an approach in which we factored the specification, used TestEra to generate abstract inputs based on one factor, and passed the results through a postprocessor that reincorporated information from the second factor. Using this technique, we were able to generate test inputs to meaningful bounds, and the inputs revealed nontrivial faults in the Galileo implementation, our specification, and our oracle. Our results suggest that BET, combined with specification abstraction and factoring techniques, could become a valuable addition to our verification toolkit and that further investigation is warranted.     

Developing a low-cost high-quality software tool for dynamicfault-tree analysis

Sophisticated modeling and analysis methods are being developed in academic and industrial research labs for reliability engineering and other domains. The evaluation and evolution of such methods based on use in practice is critical to research progress, but few such methods see widespread use. A critical impediment to disseminating new methods is the inability to produce, at a reasonable cost, supporting software tools that have the: usability and dependability characteristics that industrial users require; and evolvability to accommodate software change as the underlying analysis methods are refined and enhanced. The difficulty of software development thus emerges as a key impediment to advances in engineering modeling and analysis. This paper presents an approach to tool development that attacks these problems. Progress requires synergistic, interdisciplinary collaborations between application-domain and software-engineering researchers. The authors have pursued such an approach in developing Galileo: a fault tree modeling and analysis tool. These innovations are described in two dimensions: (1) the Galileo core reliability modeling and analysis function; and (2) the authors' work on software engineering for high-quality, low-cost modeling and analysis tools