Axiomatization
In the following several axiom schemas are listed to formalize Traceability Theory, that is used in the Electronically Controlled Air Suspension (ECAS) System case study.Reasoning about equals relation
\begin{equation*}
\vdash \forall a, b, c \in A \mid (a,b) \in equals \wedge (b,c) \in \square \to (a,c) \in \square, \text{and}\\
\vdash \forall a, b, c \in A \mid (a,b) \in equals \wedge (c,b) \in square \to (c,a) \in \square, \text{and}\\
\vdash \forall a \in A \mid (a,a) \in equals, \\
\text{where } \square \in \{ contains , requires , refines , satisfies, conflicts \}
\end{equation*}
Reasoning about requires relation
\begin{equation*}
\vdash \forall a, b, c \in A \mid (a,b) \in \square \wedge (b,c) \in requires \to (a,c) \in requires, \text{and}\\
\vdash \forall a, b, c \in A \mid (a,b) \in requires \wedge (b,c) \in \square \to (a,c) \in requires, \\
\text{where } \square \in \{ requires, refines , contains \}
\end{equation*}
Reasoning about satisfies relation
\begin{equation*}
\vdash \forall a, b, c \in A \mid (a,b) \in \square \wedge (c,b) \in satisfies \to (c,a) \in satisfies, \text{and}\\
\vdash \forall a, b, c \in A \mid (a,b) \in \square \wedge (b,c) \in satisfies \to (a,c) \in satisfies, \\
\text{where } \square = refines
\end{equation*}
Reasoning about conflicts relation
\begin{equation*}
\vdash \forall a, b, c \in A \mid (a,b) \in \square \wedge (b,c) \in conflicts \to (a,c) \in conflicts, \text{and}\\
\vdash \forall a \in A \mid (a,a) \in conflicts, \\
\text{where } \square \in \{ requires , refines , contains \}
\end{equation*}
In the following axiom schema, transitivity is used for reasoning new traces, whereas anti-symmetry and irreflexivity are used to check consistency.
\begin{equation*}
\vdash \forall a, b, c \in A \mid (a,b) \in \square \wedge (b,c) \in \square \to (a,c) \in \square, \text{and}\\
\vdash \forall a, b \in A \mid (a,b) \in \square \wedge (b,a) \in \square \to a = b, \text{and}\\
\vdash \forall a \in A \mid (a,a) \notin \square, \\
\text{where } \square \in \; \{ contains , requires , refines , satisfies \}
\end{equation*}
Consistency of \textit{contains} Relation, which is left-unique (injective relation):
\begin{equation*}
\vdash \forall a, a', b \in A \mid (a,b) \in \square \wedge (a',b) \in \square \to a = a', \\
\text{where } \square = contains
\end{equation*}
For instance, in addition to the previously defined axioms using the following axiom schema, the system detects an inconsistency between two requirements, \(r_{60}\) and \(r_{59}\) as shown in the following Table.
\begin{equation*}
\forall a, b \in A \mid (a,b) \in \square \to (a,b) \notin \triangle \wedge (b,a) \notin \triangle, \text{where} \\
\text{for each} \; \square \in \{ requires , refines , satisfies , contains , conflicts \} \text{and}\\
(requires \; \cup \; refines \; \cup \; satisfies \; \cup \; contains \; \cup \; conflicts) \setminus \square \mapsto \triangle
\end{equation*}
Some Requirements and Code Fragments in ECAS