Unique First Cause Test Generation - lgwagner/SpeAR GitHub Wiki

Unique First Cause test generation is an analysis of sorts; it analyzes the logic of a specification to produce a test suite that 1) sets each basic condition in a formula to take on all possible outcomes at least once 2) each basic condition has been shown to independently affect the formula's outcome.

The following image has a simple specification that includes three inputs a, b, and c of types boolean, integer, and real respectively. It has a single output x. This specification is total; r0 defines when x is true and r1 defines all the cases (they are the complement of r0) when x is false.

UFC test generation is performed by adding the ufc keyword between the name of a requirement and the ':' as shown in the above example. Once these annotations are made Logical Entailment analysis will generate them automatically. The tests generated will following the naming convention shown in the following image.

UFC tests will exercise each of the conditions to demonstrate that it can uniquely affect the outcome of the requirement. The UFC tests generated from the example are shown below.

Finally, users should note that UFC test generation is a prototype to demonstrate the capability but it is not necessarily ready for production. It only supports test generation over logical connectors (not, and, or, xor, implies) and pre expressions. Users interested in more broad support can leave an issue.