Meta-properties

Next: Tagged Events Up: Formal Model of Traces, Previous: Trace Properties and Refinement

Meta-properties

We classify trace properties using meta-properties. The meta-properties we need are all instances of the following schemas.
$\begin{program*} \> \\ \> R preserves P ==\\ \> \mforall{}x,y:Trace$_{\mbox{\s... ...P x)\\ \> {}\mRightarrow{} (x R y)\\ \> {}\mRightarrow{} (P y)) \end{program*}$

$\begin{program*} \> \\ \> (ternary) R preserves P ==\\ \> \mforall{}x,y,z:Trac... ...y)\\ \> {}\mRightarrow{} (R x y z)\\ \> {}\mRightarrow{} (P z)) \end{program*}$

$\begin{program*} \> \\ \> P $\rhd$\ Q ==\\ \> \mforall{}tr:\vert E\vert List\\ \> ((P tr) {}\mRightarrow{} (Q tr)) \end{program*}$
A trace property is a safety property if it is preserved by
$\begin{program*} \> \\ \> tr$_{1}$\ safetyR$_{\mbox{\small {E}}}$\ tr$_{2}$\ == tr$_{2}$\ \mleq{} tr$_{1}$\end{program*}$
A property is memoryless if it is preserved by the operation of removing all events with a given message. So memoryless properties are the ones that are preserved by
$\begin{program*} \> \\ \> L$_{1}$\ memorylessR$_{\mbox{\small {E}}}$\ L$_{2}$\ ... ... \vert \mneg{}\msubb{}(b \\ \> =msg=$_{\mbox{\small {E}}}$\ a)>) \end{program*}$
A property is send-enabled if it is preserved when a send event is appended to the trace. Send-enabled properties are the ones preserved by
$\begin{program*} \> \\ \> L$_{1}$\ send-enabledR$_{\mbox{\small {E}}}$\ L$_{2}$... ...l {E}}}$\ x))\\ \> \mwedge{} (L$_{2}$\\ \> = (L$_{1}$\ @ [x]))) \end{program*}$
A property is asynchronous if it is preserved when adjacent deliver events or adjacent send events that have different locations are swapped. Asynchronous properties are the ones preserved by
$\begin{program*} \> \\ \> asyncR$_{\mbox{\small {E}}}$\ ==\\ \> swap-adjacent$... ...> \mwedge{} (\muparrow{}(is-send$_{\mbox{\small {E}}}$\ y)))))}}}$\end{program*}$
A property is delayable if it is preserved when adjacent events, one of which is a send and the other a deliver, and which have different message content, are swapped.
$\begin{program*} \> \\ \> x R\_del$_{\mbox{\small {E}}}$\ y ==\\ \> (\mneg{}\m... ...{E}}}$\ x))\\ \> \mwedge{} is-deliver$_{\mbox{\small {E}}}$(y))) \end{program*}$

$\begin{program*} \> \\ \> delayableR$_{\mbox{\small {E}}}$\ == swap-adjacent$_{\mbox{\small {x R\_del$_{\mbox{\small {E}}}$\ y}}}$\end{program*}$
A property is composable if it is preserved when two traces, L $_{1}$ and L $_{2}$ , that have no messages in common, are appended. Composable properties are the ones preserved by the ternary realtion
$\begin{program*} \> \\ \> composableR$_{\mbox{\small {E}}}$\ L$_{1}$\ L$_{2}$\ ... ...ox{\small {E}}}$\ y)))\\ \> \mwedge{} (L = (L$_{1}$\ @ L$_{2}$)) \end{program*}$

Next: Tagged Events Up: Formal Model of Traces, Previous: Trace Properties and Refinement

Richard Eaton 2002-02-20