lunchtime edit
This commit is contained in:
parent
a40d643008
commit
b830e16e11
@ -33,7 +33,7 @@ automated systems.
|
|||||||
|
|
||||||
% No need to talk about abstraction yet, just define PLD PROPERLY
|
% No need to talk about abstraction yet, just define PLD PROPERLY
|
||||||
|
|
||||||
The Diagrams described here form the mathematical basis for a new visual and formal system
|
The diagrams described here form the mathematical basis for a new visual and formal system
|
||||||
for the analysis of safety critical software and hardware systems.
|
for the analysis of safety critical software and hardware systems.
|
||||||
\end{abstract}
|
\end{abstract}
|
||||||
}
|
}
|
||||||
@ -92,12 +92,12 @@ for the analysis of safety critical software and hardware systems.
|
|||||||
|
|
||||||
Propositional Logic Diagrams (PLDs) have been created
|
Propositional Logic Diagrams (PLDs) have been created
|
||||||
to collect and simplify fault~modes in safety critical systems undergoing
|
to collect and simplify fault~modes in safety critical systems undergoing
|
||||||
static analysis.%\cite{sccs}\cite{en61508}.
|
static analysis. %\cite{sccs}\cite{en61508}.
|
||||||
%
|
%
|
||||||
This type of analysis treats failure modes within a system as logical
|
This type of analysis treats failure modes within a system as logical
|
||||||
states.
|
states.
|
||||||
PLD provides a visual method for modelling failure~mode analysis
|
PLD's provide a visual method for modelling failure~mode analysis
|
||||||
within these systems, and aids the collection of
|
within these systems, and aid the collection of
|
||||||
common failure symptoms.
|
common failure symptoms.
|
||||||
%
|
%
|
||||||
Contrasting this to looking at many propositional logic equations directly
|
Contrasting this to looking at many propositional logic equations directly
|
||||||
@ -350,14 +350,14 @@ i.e. the contours $\mathcal{X}$ from the zone it inhabits.
|
|||||||
{
|
{
|
||||||
\definition{
|
\definition{
|
||||||
|
|
||||||
Let $\mathcal{F}$ be a function mapping a test case $t \in T$, to a proposition / logical equation $p \in P$.
|
Let $\mathcal{F_t}$ be a function mapping a test case $t \in T$, to a proposition / logical equation $p \in P$.
|
||||||
The test case $t$, inhabits the zone $\mathcal{Z}$ which is a collection of contours (the contours that enclose the test case).
|
The test case $t$, inhabits the zone $\mathcal{Z}$ which is a collection of contours (the contours that enclose the test case).
|
||||||
We can express this as
|
We can express this as
|
||||||
$$ \mathcal{F}:T \rightarrow P\;, $$
|
$$ \mathcal{F_t}:T \rightarrow P\;, $$
|
||||||
|
|
||||||
%$$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} \Lambda c $$
|
%$$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} \Lambda c $$
|
||||||
given by
|
given by
|
||||||
$$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} c \;. $$
|
$$ \mathcal{F_t}(t): p = \bigwedge_{c \in \mathcal{Z}} c \;. $$
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -370,14 +370,15 @@ $ a \wedge b \wedge c $.
|
|||||||
{
|
{
|
||||||
\definition{
|
\definition{
|
||||||
Let $\mathcal{G}$ be a function that returns a logic equation for a given $SMG$
|
Let $\mathcal{G}$ be a function that returns a logic equation for a given $SMG$
|
||||||
$fmg$ in the diagram, where an SMG is a non empty set of test cases
|
$fmg$ in the diagram, where an SMG is a non empty set of test cases.
|
||||||
% $t$ is a `test case'
|
% $t$ is a `test case'
|
||||||
|
$\mathcal{G}$ has a domain of SMG and a range of $P$ given as
|
||||||
as
|
as
|
||||||
$$ \mathcal{G}:SMG \rightarrow P_{fmg}. $$
|
$$ \mathcal{G}:SMG \rightarrow P. $$
|
||||||
|
|
||||||
The logic equation (using $oplus$ to represent exclusive-or) representing an SMG $p_{fmg}$ can be determined thus;
|
The logic equation (using $oplus$ to represent exclusive-or) representing an SMG $p_{fmg}$ is given thus;
|
||||||
|
|
||||||
$$\mathcal{G}_{fmg}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F}_{t} (t) \;) \; .$$
|
$$\mathcal{G}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F_t}_{t} (t) \;) \; .$$
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -385,8 +386,12 @@ The semantics of the diagram is the set of logic equations representing all its
|
|||||||
along with unused zones (i.e. zones that are not inhabited by SMGs).
|
along with unused zones (i.e. zones that are not inhabited by SMGs).
|
||||||
Thus the abstract representation of the diagram, becomes a list of logic equations
|
Thus the abstract representation of the diagram, becomes a list of logic equations
|
||||||
and unused available zones.
|
and unused available zones.
|
||||||
|
%
|
||||||
|
% THIS ABOVE COULD BE ANOTHER DEFINITION
|
||||||
|
|
||||||
|
\section{Context, functional groups, failure modes and symptoms}
|
||||||
|
|
||||||
|
\include{../shortfg}
|
||||||
|
|
||||||
\subsection{Symptom Collection}
|
\subsection{Symptom Collection}
|
||||||
|
|
||||||
@ -404,13 +409,21 @@ each SMG is represented by a contour.
|
|||||||
{
|
{
|
||||||
\definition{
|
\definition{
|
||||||
\label{SMGderivation}
|
\label{SMGderivation}
|
||||||
A diagram can be drawn to represent the collection of $SMG$s.
|
%A diagram can be drawn to represent the collection of $SMG$s.
|
||||||
|
The diagram $d$ represents $SMG$s as graphs of asterisks connected with joining lines.
|
||||||
A new diagram can be derived from this, replacing each SMG with a contour in the new diagram.
|
A new diagram can be derived from this, replacing each SMG with a contour in the new diagram.
|
||||||
This diagram is at one higher level of failure~mode abstraction than the diagram that
|
This diagram is at one higher level of failure~mode abstraction than the diagram that
|
||||||
it was produced from.
|
it was produced from.
|
||||||
|
This diagram is the `symptom collection' diagram derived form $d$.
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
\subsection{Derived Component}
|
||||||
|
|
||||||
|
The diagram $d$ represents the failure modes of a functional group,
|
||||||
|
with the joining lines defining the its symptom collection.
|
||||||
|
The `symptom collection' respresents the functional group
|
||||||
|
at a higher level of failure mode abstraction. It represents the
|
||||||
|
{\fg} as a higher level component, or {\textbf{derived component}}, with a defined set of failure modes.
|
||||||
|
|
||||||
\section{Example Diagrams}
|
\section{Example Diagrams}
|
||||||
|
|
||||||
@ -424,7 +437,7 @@ it was produced from.
|
|||||||
|
|
||||||
PLD diagrams are read by first looking at the test case asterisks.
|
PLD diagrams are read by first looking at the test case asterisks.
|
||||||
The test case asterisk will be enclosed by one or more contours.
|
The test case asterisk will be enclosed by one or more contours.
|
||||||
These contours are collated and used form the logical conjunction
|
These contours are collated and used to form the logical conjunction
|
||||||
equation for the test case.
|
equation for the test case.
|
||||||
These test case points thus represent the conjunctive aspects
|
These test case points thus represent the conjunctive aspects
|
||||||
of an equation defined in a PLD. Where these test cases are joined by lines;
|
of an equation defined in a PLD. Where these test cases are joined by lines;
|
||||||
@ -637,12 +650,12 @@ a software tool which assists in drawing these diagrams.
|
|||||||
|
|
||||||
The diagram \ref{fig:repeated} is converted to propositional logic by first looking at the test cases, and
|
The diagram \ref{fig:repeated} is converted to propositional logic by first looking at the test cases, and
|
||||||
the contours they are placed on thus:
|
the contours they are placed on thus:
|
||||||
$$ P = (b) $$
|
$$ P = (b) \; ,$$
|
||||||
$$ Q = (a) \wedge (c) \; .$$
|
$$ Q = (a) \wedge (c) \; .$$
|
||||||
|
|
||||||
The two test cases are joined by a the line named $R1$.
|
The two test cases are joined by a the line named $R1$.
|
||||||
we thus apply disjunction to the test cases:
|
we thus apply disjunction to the test cases:
|
||||||
$$ R1 = P \oplus Q $$
|
$$ R1 = P \oplus Q \;,$$
|
||||||
$$ R1 = b \oplus ( a \wedge c ) \; .$$
|
$$ R1 = b \oplus ( a \wedge c ) \; .$$
|
||||||
|
|
||||||
$R2$ joins two other test cases
|
$R2$ joins two other test cases
|
||||||
@ -885,7 +898,8 @@ The intention for these diagrams is that they are used to collect
|
|||||||
component faults and combinations thereof, into faults that,
|
component faults and combinations thereof, into faults that,
|
||||||
at the module level have the same symptoms.
|
at the module level have the same symptoms.
|
||||||
|
|
||||||
The act of collecting common symptoms by joining lines is seen as intuitive. % seen as BY ME ! HA !
|
The act of collecting common symptoms by joining lines is seen more intuitive
|
||||||
|
than lists of logic equations. % seen as BY ME ! HA !
|
||||||
It also neatly by-passes the problem of having test cases
|
It also neatly by-passes the problem of having test cases
|
||||||
which could inadvertently be placed into more than one $SMG$.
|
which could inadvertently be placed into more than one $SMG$.
|
||||||
Syntax checking (looking for contradictions and tautologies), as well as detecting
|
Syntax checking (looking for contradictions and tautologies), as well as detecting
|
||||||
|
Loading…
Reference in New Issue
Block a user