Tarski: A Platform for Automated Analysis of Traceability

Trace semantics is given as facts in Alloy. Facts are constraints that are assumed to always hold. They are used as axioms in constructing examples and counterexamples. The Refines, Requires and Contains trace types are defined irreflexive and antisymmetric (see Lines 26 and 27). In addition, Contains is injective (Line 25). As part of the semantics, we define how trace types are related to each other (Lines 30-49). For instance, according to the fact in Lines 30-33 where a, b and c are artifact elements, if a refines, requires or contains b, while b conflicts with c, then a also conflicts with c.