Tarski: A Platform for Automated Analysis of Traceability

Signatures define the vocabulary of a model in Alloy (see keyword sig). We use them to extend Trace-location for declaring artifact element types (see Lines 4, 9, 12, 15, 17, 21 and 24). Tarski employs some special annotations to specify artifacts' location types (Lines 8, 11, 14, 20 and 23). The location type information is later used by Tarski to create the Eclipse workspace fields to save traces assigned. For instance, Requirement is given as a text location in Line 11, while Code is given as a source code location in Line 20. New trace types are defined as binary relations in the signature fields (see Lines 5, 6, 12, and 18). For instance, in Line 18, Satisfies is declared as a new trace type between Implementation and Requirement.