Tarski: A Platform for Automated Analysis of Traceability

In Tarski, each trace-location and trace-link subject to formal analysis must be annotated with a type from the hierarchy obtained from the signature and the field declarations on the specification. For instance, several text fragments on a requirement document are annotated with artifact types. Blue markers indicate TextLocations which are not linked, whereas a red one indicates a trace-location that has at least one outgoing trace-link. Likewise, the user can create a trace-link using the wizards presented to her/him in the same direction of field declaration.