

home >
research >
contract work
SRI International: Automatic Test Generation ToolThe Need
Approach
ModelBased Development
Discussion About Technical ApproachThe 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. TVEC 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 TVEC like system of our own (or provide an engine to support TVEC 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.


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) 