AF3 has a semi-formal language to write requirements that allows to automatically generate test cases fulfilling the MCDC (Modified Condition/Decision Coverage) criterion. Such requirements specify the value of outputs based on the value of input, thus the interface (inputs / outputs) shall be clearly defined. Requirements are written using an if-then-else pattern.
For example, consider the following requirement:
Right-click on the requirement and select "Formal specification aspect", then move to the "Formal aspect" tab. This will create a component that allows to define the interface.
You can add inputs and outputs to the interface using the palette on the right-hand-side.
In order to formally define the requirement, add a "Code specification" behavior to the component (drag&drop from the palette). Double-click in the component to open the editor. The requirement shall follow the if-then-else pattern where the guard (if-part) shall refer to the inputs and the branches (then and else parts) shall be a list of assignments (one for each output) using only expressions on the inputs and constants.
Test cases can be automatically created by right-clicking on the requirement and selecting "Generate MCDC".
The test suite will be created as a child of the requirement: expand the arrow on the left of the requirement and double-click to open the test suite.