A Model-Based Approach to Testing Software for Critical Behavior and Properties

To integrate the theoretical concepts of composition and refinement with the engineering notions of software models and components, the Naval Research Laboratory has formulated a set of practical composition-based methods, with associated modeling and proof techniques, for developing critical software systems. The general approach is to develop a set of software components and to use various forms of composition to combine the components in a manner that guarantees properties of the composite system. An assumption underlying this research is that much of the software code can be generated automatically from models using automatic code generators. A problem is that the code generated by such tools still requires testing to ensure that the software delivers its critical services correctly and that the software behavior satisfies critical properties, such as safety properties. The need for testing arises in part because only some of the required code is generated automatically: Stubs are provided for code that cannot be generated automatically (for example, certain algorithms), and such code must be constructed manually. This talk describes model-based methods for developing software, and how the models and properties developed using these methods can be used as the basis for automatically constructing tests for evaluating the correctness of software code. These tests are designed to satisfy various coverage criteria, such as branch coverage. An example is presented showing how our model-based method can be used to construct a suite of tests for evaluating the software code controlling the behavior of an autonomous system.