Automated test generation for engineering applications

In test generation based on model-checking, white-box test criteria are represented as trap conditions written in a temporal logic. A model checker is used to refute trap conditions with counter-examples. From a feasible counterexample test inputs are then generated. Earlier research has demonstrated the usefulness of this approach and revealed its weakness. The major problems of applying this approach to engineering applications derive from the fact that engineering programs have an infinite state space and non-linear numerical computations. Our solution is to comdicate abstraction (which reduces the state space) with a numerical decision procedure (which supports preditraction by solving non-linear constraints) based on interval analysis. We have developed a prototype and applied it to MC/DC (Modified Condition/Decision Coverage) test case generation. We have used the prototype on a number of C modules taken from a conflict detection and avoidance system and from a Boeing 737 aut...

• Type: Conference
• Year: 2005
• Where: KBSE
• Authors: Songtao Xia, Ben Di Vito, César Muñoz
• Keywords: Feasible Counterexamples, KBSE 2005, Software Engineering, Trap Conditions