robin/Robin_PHD
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

AF comments in gmail

Browse Source
This commit is contained in:
Robin Clark 2011-03-14 14:02:54 +00:00
parent dc5562d3c0
commit 18b53aa09d
1 changed files with 100 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

172
logic_diagram/logic_diagram.tex
View File

@ -6,7 +6,9 @@
Propositional Logic Diagrams (PLD) have been designed to provide an intuitive method for visualising and manipulating Propositional Logic Diagrams (PLD) have been designed to provide an intuitive method for visualising and manipulating
a specific sub-set of logic equations, to express fault modes in Mechanical and Electronic Systems. a specific sub-set of logic equations, to express fault modes in Mechanical and Electronic Systems.
PLDs are a variant of constraint diagrams. Contours used to express PLDs are a variant of constraint diagrams. Contours used to express
sets represent failure modes and the Symptomatically merged groups sets represent failure modes and
collected common failure mode symptoms (symptomatically merged groups)
%Andrew Fish 13MAR2011 comment, explain Symtomatically merged groups
are akin to the `spiders'\cite{howse:rwsd} of constraint diagrams\cite{gil:tafocd}. are akin to the `spiders'\cite{howse:rwsd} of constraint diagrams\cite{gil:tafocd}.
%To aid hierarchical stages of fault analysis, it has been specifically developed for the purpose of %To aid hierarchical stages of fault analysis, it has been specifically developed for the purpose of
%joining conjunctive conditions with disjuctive conditions %joining conjunctive conditions with disjuctive conditions
@ -115,26 +117,26 @@ in a text editor or spreadsheet, a visual method is perceived as being more intu
%these points may be joined. %these points may be joined.
PLDs use three visual features that PLDs use three visual features that
can be combined to represent logic equations. Closed contours, test cases, and lines that can be combined to represent logic equations. Simple closed curves, asterisks and lines joining asterisks.
link test cases. %Closed contours, test cases, and lines that link test cases.
All features may be labelled, and the labels must be unique within a diagram, however contours may be repeated. All features may be labelled, and the labels must be unique within a diagram, however labelled contours may be repeated.
%Aditionally a label begining with the `$\neg$' character, applied only to a contour, represents negation. %Aditionally a label begining with the `$\neg$' character, applied only to a contour, represents negation.
%Regions defined by contours are used to represent given conjunctive logical conditions. %Regions defined by contours are used to represent given conjunctive logical conditions.
Test cases are marked by asterisks. These are used as a visual `anchor' Test~cases are marked by asterisks. These are used as a visual `anchor'
to mark a logical condition, the logical condition being defined by the contours to mark a logical condition, the logical condition being defined by the contours
that enclose the region on which the test~case has been placed. that enclose the region on which the test~case has been placed.
The contours that enclose represent conjunction. The contours that enclose represent conjunction.
Test~cases may be connected by joining lines. These lines represent disjunction (Boolean `XOR') of Test~cases may be connected by joining lines. These lines represent exclusive disjunction (Boolean `XOR') of
test~cases. test~cases.
With these three visual syntax elements, we have the basic building blocks for all logic equations possible. With these three visual syntax elements, we have the basic building blocks for all logic equations possible.
\begin{description} \begin{description}
\item Test cases - Points on the plane indicating a logical condition. \item Test cases - Points (asterisks) on the plane indicating a logical condition.
\item Conjunction - Overlapping contours \item Conjunction - Overlapping contours
\item Disjunction - Joining of named test cases. \item Exclusive Disjunction - Joining of named test~cases.
%\item Negation - Countours negatively named %\item Negation - Countours negatively named
\end{description} \end{description}
@ -163,10 +165,10 @@ The concrete definitions for PLD's and Spider Diagrams\cite{howse:sd} share many
A concrete {\em Propositional logic diagram} is a set of labelled {\em contours} A concrete {\em Propositional logic diagram} is a set of labelled {\em contours}
(closed curves) in the plane. The minimal regions formed by the closed curves (closed curves) in the plane. The minimal regions formed by the closed curves
can by occupied by `test points'. can by occupied by `test cases'.
The `test points' may be joined by joining lines. The `test cases' may be joined by joining lines.
A group of `test points' connected by joining lines A group of `test cases' connected by joining lines
is defined as a `test point disjunction' or Spider. is defined as a `test case disjunction' or Spider.
Spiders may be labelled. Spiders may be labelled.
%To differentiate these from common Euler diagram notation (normally used to represent set theory) %To differentiate these from common Euler diagram notation (normally used to represent set theory)
@ -174,11 +176,11 @@ Spiders may be labelled.
\subsection{ PLD Definition} \subsection{ PLD Definition}
%In English: %In English:
Possible elements in a PLD diagram are contours, test points and joining lines that connect test points. Possible elements in a PLD diagram are contours, test cases and joining lines that connect test cases.
{ {
\definition{A concrete PLD $d$ is a set comprising of a set of \definition{A concrete PLD $d$ is a set comprising of a set of
closed curves $C=C(d)$, a set of test points $T=T(d)$ and closed curves $C=C(d)$, a set of test cases $T=T(d)$ and
a set of test point joining lines $J=J(d)$. a set of test case joining lines $J=J(d)$.
$$d=\{C,T,J\}$$ $$d=\{C,T,J\}$$
} }
} }
@ -244,11 +246,11 @@ is non empty, then $\hat{z}$ is a concrete zone of $\hat{d}$. A zone is a union
} }
Each minimal region in the plane may be inhabited by one or more `test points'. Each minimal region in the plane may be inhabited by one or more `test cases'.
% One or more because in software the same logical conditions mean existing in the same % One or more because in software the same logical conditions mean existing in the same
% region. For electroincs or mechanical, one test point per region is % region. For electroincs or mechanical, one test case per region is
% mandatory. How to describe ????? % mandatory. How to describe ?????
Each test point can be associated with the set of contours that enclose it. Each test case can be associated with the set of contours that enclose it.
%defined the minimal region it inhabits. %defined the minimal region it inhabits.
{ {
@ -257,7 +259,7 @@ associating a test-point with a set of contours in the plane. This corresponds t
} }
} }
Pairs of test points may be joined by joining lines. Pairs of test cases may be joined by joining lines.
The operator $\stackrel{join}{\leftrightarrow}$ is used to The operator $\stackrel{join}{\leftrightarrow}$ is used to
show that two points are joined by a line in the concrete diagram. show that two points are joined by a line in the concrete diagram.
@ -265,120 +267,144 @@ show that two points are joined by a line in the concrete diagram.
\definition{ \definition{
$ \mathcal{F}_{j}$ is a function $ \mathcal{F}_{j}$ is a function
associating a joining line with a pair of test points. The Join t1,t2 is defined as associating a joining line with a pair of test cases. The Join t1,t2 is defined as
%$$ \mathcal{F}_{d}:J(d)\rightarrow \{t1,t2\ | t1 \in T(d) \wedge t2 \in T(d) \wedge t1 \neq t2 %\wedge t1 \stackrel{join}{\leftrightarrow} t2\} $$ %$$ \mathcal{F}_{d}:J(d)\rightarrow \{t1,t2\ | t1 \in T(d) \wedge t2 \in T(d) \wedge t1 \neq t2 %\wedge t1 \stackrel{join}{\leftrightarrow} t2\} $$
$$ \mathcal{F}_{d}:J(d)\rightarrow \{t1,t2\ | t1 \in T(d) \wedge t2 \in T(d) \wedge t1 \neq t2 \} $$ $$ \mathcal{F}_{j}:J(d)\rightarrow \{t_1,t_2\ | t_1 \in T(d) \wedge t_2 \in T(d) \wedge t_1 \neq t_2 \} $$
} }
} }
%In English: %In English:
Test points on the concrete diagram pair-wise connected by a `joining line' Test points on the concrete diagram pair-wise connected by a `joining line'
The graph formed by test~cases connected by joining lines is called an $SMG$.
A collection of test points connected by joining lines, is an Symptom Merged Group, $SMG$ %A collection of test cases connected by joining lines, is an Symptom Merged Group, $SMG$
or `test point disjunction'. The $SMG$ is the analog of the Spider in spider/constraint diagrams\ref{howse:sd}. %or `test case disjunction'.
An $SMG$ has members which are test points. The $SMG$ is the analog of the Spider in spider/constraint diagrams\ref{howse:sd}.
An $SMG$ can be considered to be a collection of test~cases.
{ {
\definition{ \definition{
%A spider is a set of test points where, %A spider is a set of test cases where,
%a test point is a member of a spider where it can trace a path connected by joining lines %a test case is a member of a spider where it can trace a path connected by joining lines
%to another member of the spider. A singleton test point can be considered a spider. %to another member of the spider. A singleton test case can be considered a spider.
Let d be a PLD : An $SMG$ is a maximal set of test points in d where
the test points belong to a sequence connected by joining lines such that:
$$ t_i \stackrel{join}{\leftrightarrow} t_n, for \; i = 1, ..., n $$
OR consider an $SMG$ as a tree whose nodes are test points. %Let d be a PLD : An $SMG$ is a maximal set of test cases in d where
%the test cases belong to a sequence connected by joining lines such that:
%$$ t_i \stackrel{join}{\leftrightarrow} t_n, for \; i = 1, ..., n $$
%OR consider an $SMG$ as a tree whose nodes are test cases.
Let d be a PLD : An $SMG$ is a collection of test~cases in d where
the test~cases belong to a graph connected by joining lines.
} }
} }
A singleton test point can be considered a sequence of one test point and is therefore also an $SMG$. A singleton test case can be considered a sequence of one test case and is therefore also an $SMG$.
% \subsection{Abstract Description of PLD} % \subsection{Abstract Description of PLD}
%and create a %and create a
% %
% An Abstract PLD {\em Propositional logic diagram} consists of contours $C$ defining zones $Z$, test points $T$ (which % An Abstract PLD {\em Propositional logic diagram} consists of contours $C$ defining zones $Z$, test cases $T$ (which
% are defined by the zone they inhabit) and pair wise connections $W$, which connect test points. % are defined by the zone they inhabit) and pair wise connections $W$, which connect test cases.
% Collections of test points, linked by shared conecting lines, form a set of test point groups $G$. % Collections of test cases, linked by shared conecting lines, form a set of test case groups $G$.
% %
% A Zone defined by the contours that enclose it in the concrete diagram. % A Zone defined by the contours that enclose it in the concrete diagram.
% %
% $$ Z \subseteq C $$ % $$ Z \subseteq C $$
% %
% A test point $t \in T$ in habits a zone on the diagram. % A test case $t \in T$ in habits a zone on the diagram.
% %
% $$ \eta(t) = Z $$ % $$ \eta(t) = Z $$
% %
% A joining line $$ w \in W $$ joins test points. % A joining line $$ w \in W $$ joins test cases.
% %
% $$ w = t1 \stackrel{join}{\rightarrow} t2 | t1 \neq t2 \wedge t1 \in T \wedge t2 \in T $$ % $$ w = t1 \stackrel{join}{\rightarrow} t2 | t1 \neq t2 \wedge t1 \in T \wedge t2 \in T $$
% %
% A test point group $g \in G$ is defined by test points linked by shared connecting lines. % A test case group $g \in G$ is defined by test cases linked by shared connecting lines.
\subsection{Semantics of PLD} \subsection{Semantics of PLD}
\begin{itemize} \begin{itemize}
\item A closed curve in a PLD represents a condition (logical state) being modelled. \item A closed curve in a PLD represents a condition (logical state) being modelled.
\item A test point represents the conjunction of the conditions represented by the curves that enclose it. \item A test case represents the conjunction of the conditions represented by the curves that enclose it.
\item A $SMG$ represents the disjunction of all test points that are members of it. \item A $SMG$ represents the exclusive disjunction of all test cases that are members of it.
\end{itemize} \end{itemize}
To obtain the set of propositions from a PLD, each $SMG$ must be traversed To obtain the set of propositions from a PLD, each $SMG$ must be traversed
along each joining line. For each test case along each joining line. For each test case
in the $SMG$ a new section of the equation is disjunctively appended to it. in the $SMG$ a new section of the equation is exclusive-disjunctively appended to it.
% %
Let conjunctive logic equation associated with a test point Let conjunctive logic equation associated with a test case
be determined from the contours that enclose it. be determined from the contours that enclose it.
i.e. the contours $\mathcal{X}$ from the zone it inhabits. i.e. the contours $\mathcal{X}$ from the zone it inhabits.
{ {
\definition{ \definition{
Let $\mathcal{F}_{t}$ be a function mapping a test point to a proposition / logical equation $p \in P$. Let $\mathcal{F}$ be a function mapping a test case $t \in T$, to a proposition / logical equation $p \in P$.
The test point inhabits the zone $\mathcal{Z}$ which is a collection of contours (the contours that enclose the test point. 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
$$ \mathcal{F}:T \rightarrow P $$ $$ \mathcal{F}: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
$$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} c $$ $$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} c \;. $$
} }
} }
In English: %In English:
Thus a `test point' enclosed by contours labelled $a,b,c$ would be represented by the logic equation Thus a `test case' enclosed by contours labelled $a,b,c$ would be representing the logic equation
$ a \wedge b \wedge c $. $ a \wedge b \wedge c $.
{ {
\definition{ \definition{
Let $\mathcal{G}_{fmg}$ 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 points $fmg$ in the diagram, where an SMG is a non empty set of test cases
% $t$ is a `test point' % $t$ is a `test case'
as
$$ \mathcal{G}:SMG \rightarrow P_{fmg}. $$
$$ \mathcal{G}:SMG \rightarrow P_{fmg} $$ 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}$ can be determined thus. $$\mathcal{G}_{fmg}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F}_{t} (t) \;) \; .$$
$$\mathcal{G}_{fmg}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F}_{t} (t) \;) $$
} }
} }
The abstract PLD diagram is a set of logic equations representing all SMGs, The semantics of the diagram is the set of logic equations representing all its SMGs,
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
and unused available zones.
\subsection{Symptom Collection}
The methodology using these propositional logic diagrams is concerned with
taking functional groups of components, and representing the failure
modes of those components as countours in the diagram.
The test cases, when analysed can be grouped into $SMG$s which
define the failure mode behaviour of the functional group.
As we may be interested in treating the functional group
and a component to model higher levels of design, or failure mode abstraction,
we can derive a new diagram from the $SMG$s. Each $SMG$ represents a failure
mode of the functional group, therefore in the higher level diagram
each SMG is represented by a contour.
{ {
\definition{ \definition{
\label{SMGderivation} \label{SMGderivation}
A diagram can be reduced to a collection of $SMG$s. A diagram can be drawn to represent the collection of $SMG$s.
A new diagram can be derived from this, replacing a contour for each SMG. A new diagram can be derived from this, replacing each SMG with a conour in the new diagram.
This diagram is at one higher level of abstraction then 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.
} }
} }
@ -389,7 +415,12 @@ it was produced from.
\subsection {How to read a PLD diagram} \subsection {How to read a PLD diagram}
PLD diagrams are read by first looking at the test case points. #
#
# 14MAR2011 14:02 up to here looking though andrews comments
#
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 collected and form the logical conjunction These contours are collected and form the logical conjunction
equation for the test case. equation for the test case.
@ -854,19 +885,16 @@ Some deterministic based safety standards are specifying
that not only single component failure modes must be considered in that not only single component failure modes must be considered in
analysis, but that the possibility of two component failing analysis, but that the possibility of two component failing
simultaneously must be considered. simultaneously must be considered.
%<<<<<<< HEAD
%EN298 states that if a burner controller is in `lock out' (i.e. has detected a fault
%and has ordered a shutdown) a secondary fault cannot be allowed to put the equipment under control (the burner) into a dangerous state.
%To cover this rigorously, we are bound to consider more than one fault being active at a time.
%=======
European Norm EN298~\cite{en298}[Sn.9] states that if a burner controller is in `lock out' (i.e. has detected a fault European Norm EN298~\cite{en298}[Sn.9] states that if a burner controller is in `lock out' (i.e. has detected a fault
and has ordered a shutdown) a secondary fault cannot be allowed to put the equipement under control (the burner) into a dangerous state. and has ordered a shutdown) a secondary fault cannot be allowed to put the equipement under control (the burner) into a dangerous state.
To cover this rigorously, we must consider all faults that can lead to a LOCKOUT condition To cover this rigorously, we must consider all faults that can lead to a LOCKOUT condition
and then look for others that could put the system into a dangerous state after the LOCKOUT. and then look for others that could put the system into a dangerous state after the LOCKOUT.
In practise, this would be a gigantic (as probably impossible task). In practise, this would be a gigantic (as probably impossible task).
iWhat we can consider though, are all faults being double simultaneous in the FMMD What we can consider though, are all faults being double simultaneous in the FMMD
methodology, because we need only look for the double faults within each functional group. methodology, because we need only look for the double failure modes within each functional group.
%>>>>>>> c066ba127e610f62789d083a0be3eaa9f6b7a427 Because we are looking for double failure modes within small groups
the number of checks cross product factor is drastically reduced.
So drastically reduced that it makes it a practical possibility.
\paragraph{Covering Double faults in a PLD Diagram} \paragraph{Covering Double faults in a PLD Diagram}
Because we are allowed to repeat contours in a PLD diagram, Because we are allowed to repeat contours in a PLD diagram,
we can arrange them in a matrix like configuration as in figure \ref{fig:doublesim}. we can arrange them in a matrix like configuration as in figure \ref{fig:doublesim}.