Skip past navigation NASA Langley Formal Methods



quick page






  home > research > contract work

SRI International: Automatic Test Generation Tool

The Need

  • Testing accounts for more than half of the development costs in much software development
  • Generation of test cases is mostly done by hand and is tedious and error-prone
  • We are going to automate test-case generation using formal methods


  • We target embedded systems
    • Regulatory frameworks require massive testing to specific coverage criteria
    • Recent shift to model-based development provides the technical hooks we need
  • Specific focus: Matlab (Simulink/Stateflow)
    • For real-time applications
    • Building prototype test generator

Model-Based Development

  • This is the key enabler
  • Gives access to early-lifecycle descriptions that we can analyze (Previously, all you had was English and code)
  • Matlab is dominant overall
  • But others rule the aerospace niche: Scade/Esterel, StateMate, Spark, Beacon

Discussion About Technical Approach

The goal is to check that the code behaves as it should. Since the implementation code implements the discrete controller, unit testing does not require the continuous environment. The approach is to generate test vectors off the specification of the discrete controller and pump them into the implementation to make sure it produces the same output as the specification. The code is instrumented so you can measure coverage and the goal is to achieve MCDC structural coverage. Methods of test case generation are based on targeting coverage of the specification. Ww are deliberately not generating test vectors from the code. The idea is that if you cover the specification adequately, then you should have also covered the code. If not, then the code contains "unintended function" which should be removed.. Coverage of the specification can consider either the domains of its inputs, or its control structure. T-VEC does domain coverage. It collects all constraints on the domains of its input variables (e.g., x>=5, x+y > 6) and propagates these to saturation, then picks off cases that target the extreme and middle values of each variable. ICS already does this constraint propagation, so we could easily build a T-VEC like system of our own (or provide an engine to support T-VEC itself). Covering the control structure can be done using model checking: structural coverage can be formulated as CTL or LTL properties; counterexamples to the negation of these properties are then test cases. Of course we need to work with the model checker so that it generates a fresh counterexample each time. Classical symbolic model checkers require that arithmetic constraints be abstracted to uninterpreted propositions, which can lead to infeasible test cases. Explicit state can handle the arithmetic, and so can bounded model checking with ICSAT.


  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 11 January 2002 (10:21:43)