Robin_PHD/logic_diagram/logic_diagram.tex

\ifthenelse {\boolean{paper}}
{
\begin{abstract} 
%This chapter describes using diagrams to represent propositional logic.
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.
PLDs are a variant of constraint diagrams. Contours used to express 
sets represent failure modes 
and 
collected common failure mode symptoms (symptomatically merged groups (SMG))
%Andrew Fish 13MAR2011 comment, explain Symtomatically merged groups
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 
%joining conjunctive conditions with disjuctive conditions
%to group the effects of failure modes.
PLD Diagrams can also be used to model the structure of software
and the flow of data through a computer program. 
This type of diagram can therefore
integrate logical models from mechanical, electronic and software domains.
Nearly all modern safety critical systems involve these three disciplines.
%
It is intended to be used for analysis of automated safety critical systems.
Many types of safety critical systems now legally 
require fault mode effects analysis\cite{sccs}[pp 38-39],
but few formal systems exist and wide-spread take-up is
not yet the norm\cite{safeware}. 
%
Because of its visual nature, it is easy to manipulate and model
complicated conditions that can lead to dangerous failures in 
automated systems.

% 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
for the analysis of safety critical software and hardware systems.
\end{abstract}
}
{
\section{Intrduction}
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.
PLDs are a variant of constraint diagrams. Contours used to express 
sets represent failure modes and the symptomatically merged groups (SMG)
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 
%joining conjunctive conditions with disjuctive conditions
%to group the effects of failure modes.
PLD Diagrams can also be used to model the structure of software
and the flow of data through a computer program. 
This type of diagram can therefore
integrate logical models from mechanical, electronic and software domains.
Nearly all modern safety critical systems involve these three disciplines.
%
It is intended to be used for analysis of automated safety critical systems.
Many types of safety critical systems now legally 
require fault mode effects analysis\cite{sccs}[pp 38-39],
but few formal systems exist to assist in this, and wide-spread take-up is
not yet the norm.\cite{sccs}[pp 304-305]. 
%
Because of its visual nature, it is easy to manipulate and model
complicated conditions that can lead to dangerous failures in 
automated systems.

% 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
for the analysis of safety critical software and hardware systems.
}

%\title{Propositional Logic Diagrams}
%\begin{keyword}
%  fault~tree fault~mode EN298 EN61508  EN12067  EN230 UL1998 safety~critical logic euler venn propositional
%\end{keyword}
%\end{frontmatter}

% In software looking at one condition means lots of dont care situations
% in static analysis we look at given sub-sets of faults and assume the other faults
% are not active.
% This is a major cultural difference !
% it deserves a whole chapter.


\ifthenelse {\boolean{paper}}
{
\section{Introduction}
}
{

}

Propositional Logic Diagrams (PLDs) have been created
to collect and simplify fault~modes in safety critical systems undergoing
static analysis. %\cite{sccs}\cite{en61508}.
%
This type of analysis treats failure modes within a system as logical
states.  
PLD's provide a visual method for modelling failure~mode analysis
within these systems, and aid the collection of
common failure symptoms.
%
Contrasting this to looking at many propositional logic equations directly
in a text editor or spreadsheet, a visual method is perceived as being more intuitive.


%Traditional set theory is often represented by Euler\cite{euler} or Spider\cite{spider}
%diagrams. These use contours to describe inclusion in a set.may be merged and create a  
%Propositional Logic Diagrams (PLDs) use named contours represent a logical conditions.
%Where an Euler diagram would use
%overlapping contours to represent inclusion in sets,
%PLDs use these to represent conjunction of the conditions.

%Named reference points may be placed onto the diagram,
%these represent test cases for conjunction. 
%These can be joined by lines to apply disjunction.
%In a spider diagram the lines would represent that the object represented coul;d belong to either set.
%in a PLD it means that the logical conditions represent disjuction; a boolean OR condition.
%these points may be joined. 

PLDs use three visual features that
can be combined to represent logic equations. Simple closed curves, asterisks and lines joining asterisks.
%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 labelled contours may be repeated.
%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.

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
that enclose the region on which the test~case has been placed.
The contours that enclose represent conjunction.
Test~cases may be connected by joining lines. These lines represent exclusive disjunction (Boolean `XOR') of
test~cases.

With these three visual syntax elements, we have the basic building blocks for all logic equations possible.
\begin{description}
\item Test cases - Points (asterisks) on the plane indicating a logical condition.
\item Conjunction - Overlapping contours
\item Exclusive Disjunction - Joining of named test~cases.
%\item Negation - Countours negatively named
\end{description}

% Because of this
% we have the complete suite of logical primitives here, conjunction, disjuction and negation.
% Form these complex logic equations can be respresented in 2D.

% Another advantage of this is being able to describe `don't care' conditions.
% Very often in digital hardware design, or in a computer program
% many logical conditions are  `don't care'.
% These are difficult to specify in set theory.
 



\section{Formal Description of PLD}

Definitions of concrete and abstract PLD's follow.
Well-formedness conditions for PLD's are separated from this definition, because of 
practical differences between the way they are used to represent software as opposed to
representing electronics and mechanical systems.
The concrete definitions for PLD's and Spider Diagrams\cite{howse:sd} share many common features.


\subsection{Concrete PLD Definition}

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
can by occupied by `test cases'.
The `test cases' may be joined by joining lines.
A group of `test cases' connected by joining lines
is defined as a `test case disjunction' or Spider.
Spiders may be labelled.

%To differentiate these from common Euler diagram notation (normally used to represent set theory)
%the curves are drawn using dotted and dashed lines.

\subsection{ PLD Definition}
%In English:
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 
closed curves $C=C(d)$, a set of test cases $T=T(d)$ and 
a set of test case joining lines $J=J(d)$.
 $$d=\{C,T,J\}$$
}
}

%In English:
Each element of  the diagram has a unique label within the diagram.
%Thus the set of labels found in a diagram is 
%a subset of the powerset of characters that can be present in a label.

%{
%\definition{ $ \mathcal{F}_{d}:C(d) \rightarrow  \mathcal{P}\Lambda$ is a 
%function associating a label drawn from an infinite 
%set of labels $\Lambda$.
%}
%}

%In English:
%A minimal region of a PLD diagram d is a 
%region bounded by curves.
%connected component of $\mathbb{R}^{2} - \; \bigcup_{c \in C(d)} c$

%That is to say the complement of all other regions is subtracted from the plane.
%- Or in another way- that smallest area defined by the curves that enclose it


%% \hat is used to indicate CONCRETE

{
\definition{
  A minimal region of concrete PLD diagram d is a connected component of  

$$ \mathbb{R}^{2} - \; \bigcup_{\hat{c} \in \hat{C}(\hat{d})}\hat{c}$$

% I.e. The contours break the connectivity
}
}

{
\definition
{
  Let d be a PLD and $ \mathcal{X} \subseteq \hat{C}(\hat{d})$ a set of contours.
 If the set
$$ \hat{z} =  \bigcap_{c \in \mathcal{X}} 
             {interior} 
             (\hat{c}) 
             \; \cup \;
              \bigcap_{\hat{c} \in \hat{C}-X} 
             exterior (\hat{c}) 
$$

is non empty, then $\hat{z}$ is a concrete zone of $\hat{d}$. A zone is  a union of minimal regions. The set of all concrete zones of $\hat{d}$
 is denoted $ \hat{\mathcal{Z}} $. 

% NOT interested in labelling the zones.
% but am interested in  
%The set of labels associated with the contours in $\mathcal{X}$ is the zone label set $\hat{\mathcal{Z}}(\hat{z})$
%of $\hat{z}$.
%$$ \hat{\mathcal{L}}(\hat{z}) = \bigcup_{\hat{c} \in \mathcal{X}} \mathcal{F}_{d}(\hat{c}) $$
%
% So Z is the set of all available for use ZONES; great !

}
}


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 
% region. For electroincs or mechanical, one test case per region is
% mandatory. How to describe ?????
Each test case can be  associated with the set of contours that enclose it.
%defined the minimal region it inhabits.

{
\definition{ $ \mathcal{Z}_{d}:T(d)\rightarrow \mathcal{C}$ is a function 
associating a test-point with a set of contours in the plane. This corresponds to the interior of the contours defining the zone.
}
}

Pairs of test cases may be joined by joining lines.
The operator $\stackrel{join}{\leftrightarrow}$ is used to
show that two points are joined by a line in the concrete diagram.

{
\definition{
 
$ \mathcal{F}_{j}$ is a function 
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}_{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:
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 cases connected by joining lines, is an  Symptom Merged Group, $SMG$
%or `test case disjunction'. 
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{ 
%A spider is a set of test cases where, 
%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 case can be considered a spider. 


%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 case can be considered a sequence of one test case and is therefore also an $SMG$.


% \subsection{Abstract Description of PLD}
%and create a  
% 
% 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 cases.
% 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.
% 
% $$ Z \subseteq C $$
% 
% A test case $t \in T$ in habits a zone on the diagram.
% 
% $$ \eta(t) = Z $$
% 
% 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 $$
% 
% A test case group $g \in G$ is defined by test cases linked by shared connecting lines.


\subsection{Semantics of PLD}

\begin{itemize}
\item A closed curve in a PLD represents a condition (logical state) being modelled.
\item A test case represents the conjunction of the conditions represented by the curves that enclose it. 
\item A $SMG$ represents the exclusive disjunction of all test cases that are members of it.
\end{itemize}

To obtain the set of propositions from a PLD, each $SMG$ must be traversed
along each joining line. For each test case
in the $SMG$ a new section of the equation is exclusive-disjunctively appended to it.
%
Let conjunctive logic equation associated with a test case
be determined from the contours that enclose it.
i.e. the contours $\mathcal{X}$ from the zone it inhabits.

{
\definition{
 
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).
We can express this as
$$ \mathcal{F}_{t}:T \rightarrow P\;, $$

%$$ \mathcal{F}(t): p  = \bigwedge_{c \in \mathcal{Z}}  \Lambda c  $$  
given by
$$ {F}_{t}(t): p  = \bigwedge_{c \in \mathcal{Z}}  c \;. $$
}
}



%In English:
Thus a `test case' enclosed by contours labelled $a,b,c$ would be representing the logic equation
$ a \wedge b \wedge c $.

{
\definition{
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. 
%  $t$ is a `test case'
$\mathcal{G}$ has a domain of SMG and a range of $P$ given as
as
$$ \mathcal{G}:SMG \rightarrow P. $$

The logic equation (using $oplus$ to represent exclusive-or) representing an SMG $p_{fmg}$ is given thus;

$$\mathcal{G}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F}_{t} (t) \;) \; .$$
}
}

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).
Thus the abstract representation of the diagram, becomes a list of logic equations
and unused available zones.
%
% THIS ABOVE COULD BE ANOTHER DEFINITION

\section{Context, functional groups, failure modes and symptoms}

The intended application of these diagrams, is to model failure modes
of collection of components, or {\fgs}. The aim is to
create a derived component that represents the {\fg}.
PLD diagrams are designed to aid this process.
% Asterisks represent combinations of failure 
%modes. These are failure mode scenarios, or `test~cases'.

\input{shortfg}

\subsection{Symptom Collection}

\paragraph{Failure Mode Modular De-Composition (FMMD).}
The methodology using these propositional logic diagrams is concerned with
taking functional groups of components, analysing how the functional group
can fail, and then deriving a failure mode model for the functional group
so that we can treat it as a component in its own right, or as a `derived component'

\paragraph{From component failure modes to {\fg} failure modes.}
We represent the failure
modes of the components within a {\fg} as contours in the diagram.
The test cases represent combinations of component failure modes
within the functional group. These are drawn as asterisks on the diagram.
%
The test cases, when analysed can be grouped into $SMG$s.
The $SMG$, Symptomatically merged group, is a collection of test
cases where their failure symptoms, from the perspective of the {\fg}, is the same.
%
Each $SMG$
defines a failure mode behaviour of the functional group as though the
{\fg} were considered as a high level component.
%
As we may be interested in treating the functional group
as a {\dc} 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{
\label{SMGderivation}
%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.
This diagram is at one higher level of failure~mode abstraction than the diagram that
it was produced from.
This diagram is the `symptom collection' diagram derived form $d$.
}
}

\paragraph{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' represents the functional group
at a higher level of failure mode abstraction. That is to say,
the contours in the new diagram represent the ways in which the {\fg} considered
as an entity can fail. The new represents the 
{\fg} as a higher level component, or {\textbf{derived component}}, with its own set of failure modes.

\ifthenelse {\boolean{paper}}
{
% ref symptom extraction process paper HERE
}
{
Chapter \ref{chap:sympex} describes the symptom abstraction process, detailing algorithms and 
validation and consistency checks applied.
}


\section{Example Diagrams}


\subsection {How to read a PLD diagram}

%#
%#
%# 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.
These contours are collated and used to form the logical conjunction 
equation for the test case. 
These test case points thus represent the conjunctive aspects
of an equation defined in a PLD. Where these test cases are joined by lines;
these represent disjunction of the conjunctive aspects defined by the test cases.
Joining lines thus represent exclusive disjunction in a PLD.

%Where negation and assertion of a logical condition is required in the same diagram, a separate contour can be created, which is 
%..assigned the same name as its positive counter part, but preceded by a negation `$\neg$' sign.
%Obviously were a drawing to show conjunction of a contour and its complement
%this would result in a contradiction for any test case placed on it, and would be a visual `syntax error'. 

%Note that negation is handled explicitly. This is to allow `don't care'
%conditions. Should a test case be outside a contour, that contour is a `don't care' condition.
%In a PLD, contours may be represented in complement, to provide
%logical negation. Here the contour name is begun with the negation symbol `$\neg$'.
%%To represent conjunction of logical conditions (Boolean `AND'), contours may be overlapped.

%Providing explicit negation, in addition to disjunction and conjunction
%allows us to represent `don't care' or `tri-state' logical conditions. Simply by
%not using the conditions we are not interested in they are `don't care'.
%

%\section{Example Logic Diagrams}

\subsection{ Logical AND example }
\begin{figure}[h]
 \centering
 \includegraphics[width=150pt]{logic_diagram/ldand.jpg}
 % ldand.jpg: 279x247 pixel, 72dpi, 9.84x8.71 cm, bb=0 0 279 247
 \caption{PLD diagram Example Logical AND}
 \label{fig:ld_and}
\end{figure}


In the diagram \ref{fig:ld_and} the area of intersection between the contours $a$ and $b$
represents the conjunction of those conditions. The point $P$ represents the logic equation
$$ P = (a \wedge b) $$
There are no  joining lines % and so this diagram represents one equation only, $ P = (a \wedge b) $.
and this diagram represents an $SMG$ with one element. %, $ (a \wedge b) $

\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, this could be considered to be a functional~group with two failure states $a$ and $b$.
The proposition $P$ considers the scenario where both failure~modes are active.

For base component level analysis, this would be considering two base component failures
simultaneously. At higher levels of failure mode abstraction, this could represent
sub-system failures, for instance two fuel shutdown safety valves failing to close.
% if paper
%  more detail
% if chapter
% reference gas shutoff valve closure example
%

%\clearpage
\subsection { Logical XOR example }

\begin{figure}[h]
 \centering
 \includegraphics[width=250pt,keepaspectratio=true]{logic_diagram/ldor.jpg}
 % ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
 \caption{Logical XOR example PLD diagram}
 \label{fig:ld_or}
\end{figure}

% \begin{figure}[h]
%  \centering
%  \includegraphics[width=250pt]{logic_diagram/ldor.jpg}
%  % ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
%  \label{fig:ld_or}
%  \caption{Logical XOR example PLD diagram}
% \end{figure}

% \begin{figure}[h+]
% %\centering
% %\input{ldor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldor.jpg}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.60]{ldor.eps}
% \caption{Logical OR}
% \label{fig:ld_or}
% \end{figure} % OR


The diagram \ref{fig:ld_or} is converted to propositional logic by first looking at the test cases, and 
the zones they are placed in. 
$$ P = (a) $$ 
$$ Q = (b) $$  

The two test cases are joined by a the line named $R$.
We thus apply exclusive disjunction to the test cases:
$$ R = P \oplus Q \; . $$ 
substituting the test cases for their propositional logic equations gives
\begin{equation}
 R = ((a) \oplus (b)) \; .
\label{eqn:l_or}
\end{equation}

\paragraph{Failure Analysis Interpretation}
Equation \ref{eqn:l_or} would be interpreted to mean that
either failure mode a or b occurring, would have the same failure symptom for the circuit/functional~group
under analysis.



%\clearpage
\subsection {Labels and usage}

%In diagram \ref{fig:ld_meq} Z and W were labelled but were not necessary for the final expression
%of $ R = b \vee c $. The intended use of these diagrams, is that resultant logical conditions be used in a later stage of reasoning.
%Test cases joined by disjunction, all become represented in one, resultant equation.
%Therefore only test cases not linked by any disjunctive joining lines need be named.
%
%The diagram   \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with 
%two unnamed test cases.

Diagram \ref{fig:ld_meq2} 
shows three test~cases, Q, R and P.

Z and W were labelled but this was not necessary for determination of the final expression
of $ R = b \oplus c $. 
%The intended use of these diagrams, is that resultant logical conditions be used in a later stage of reasoning.
%Test cases joined by disjunction, all become represented in one, resultant equation.
%Therefore only test cases not linked by any disjunctive joining lines need be named.
%The diagram   \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with 
%two unnamed test cases.

\begin{figure}[h]
 \centering
 \includegraphics[width=250pt,keepaspectratio=true]{logic_diagram/ldmeq2.jpg}
 % ldmeq2.jpg: 572x297 pixel, 72dpi, 20.18x10.48 cm, bb=0 0 572 297
 \caption{Labels in PLD diagrams}
 \label{fig:ld_meq2}
\end{figure}
% 
% \begin{figure}[h]
%  \centering
%  \includegraphics[bb=0 0 572 297,scale=0.7,keepaspectratio=true]{logic_diagram/ldmeq2.jpg}
%  % ldmeq2.jpg: 572x297 pixel, 72dpi, 20.18x10.48 cm, bb=0 0 572 297
%  \label{fig:ld_meq2}
%  \caption{Labels in PLD diagrams}
% \end{figure}

% 
% \begin{figure}[h+]
% %\centeringeragraph
% %\input{millivolt_sensor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{logic_diagram/ldmeq2.jpg}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.4]{ldmeq2.eps}
% \caption{Several Logical Expressions with unamed test cases}
% \label{fig:ld_meq2}
% \end{figure}


% \tiny
\vspace{0.3cm}
 \begin{tabular}{||c|c|l||} \hline \hline
   {\em $SMG$ }  & {\em Failure Mode equation } &  {\em comments  }      \\ \hline
       Q         &  $(a)$           &    Symptom Q is active when fault mode `a` is     \\ \hline
       P         &  $(b \wedge c)$    &  Symptom P is active when `$b \wedge a$' is     \\ \hline
       R         &  $(b \oplus c)$  &    Symptom R is active when either `b' or `c' is     \\ \hline
      % T         &  T  &    T     \\ \hline \hline
 \end{tabular}
\vspace{0.3cm}
% \normalsize

\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, this could be considered to be a functional~group with three failure states $a$,$b$ and $c$.
It has three SMG's Q,R and P. Thus there are three ways in which this functional~group is considered to fail.

%\clearpage



\subsection { Contours with shared label example }


Contours/Closed Curves with the same label are allowed in a PLD diagram.
Logical contradictions or tautologies can be detected automatically by
a software tool which assists in drawing these diagrams.

\begin{figure}[h]
 \centering
 \includegraphics[width=300pt,bb=0 0 560 195,keepaspectratio=true]{./logic_diagram/repeated.jpg}
 % repeated.jpg: 560x195 pixel, 72dpi, 19.76x6.88 cm, bb=0 0 560 195
 \caption{Contours may share labels in a PLD}
 \label{fig:repeated}
\end{figure}

% 
% \begin{figure}[h]
%  \centering
%  \includegraphics[bb=0 0 485 206]{logic_diagram/repeated.jpg}
%  % repeated.jpg: 539x229 pixel, 80dpi, 17.11x7.27 cm, bb=0 0 485 206
%  \label{fig:repeat}
% \end{figure}

%  \begin{figure}[h]
%  \centering
%  \includegraphics[bb=0 0 486 206]{./repeated.jpg}
%  % repeated.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 486 206
%  \label{fig:repeated}
% \end{figure}



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: 
$$ P = (b) \; ,$$ 
$$ Q = (a) \wedge (c) \; .$$  

The two test cases are joined by a the line named $R1$.
we thus apply disjunction to the test cases:
$$ R1 = P \oplus Q \;,$$ 
$$ R1 = b \oplus ( a \wedge c ) \; .$$

$R2$ joins two other test cases
$$R2 = a \oplus c \; .$$

The test~case $R3$ (residing in the intersection of contours $a$ and $a$)
represents the logic equation $R3 = a \wedge b$.

\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, $R2$ is the symptom of either failure~mode $a$ or $c$
occurring. $R1$ is the symptom of $b$ exclusive-or $a \wedge c$ occurring.
The third SMG %or  symptom 
shown is test case $R3$ (representing equation $a \wedge b$).
This diagram is incomplete, there is no test case for the fault mode $a$.
The `available region' $a \backslash b$ (i.e. the area defined by contour $a$ excluding contour $b$) has no test case, 
and this would be considered a `syntax error'
by the FMMD software tool.



%\clearpage


\pagebreak[3]
\subsection { Inhibit Failure }

%
% very interesting here Inhibit is ENCLOSURE and simultaneous faults are PURE INTERSECTION
%


Very often a failure mode can only occur given a pre-condition.
This could be the previous failure of some other component or a specific environmental condition.
In Fault Tree Analysis (FTA) this pre-condition to a given failure~mode,
is represented by an inhibit gate.\cite{nasafta}[pp41-42],\cite{nucfta}.
 
\begin{figure}[h]
 \centering
 \includegraphics[width=320pt,keepaspectratio=true]{logic_diagram/inhibit.jpg}
 % inhibit.jpg: 404x252 pixel, 80dpi, 12.83x8.00 cm, bb=0 0 364 227
 \caption{Conditional failure modes: PLD inhibit gate diagram}
 \label{fig:inhibit}
\end{figure}



The diagram \ref{fig:inhibit} has a test case in the contour $C$.
Contour $C$ is \textbf{enclosed} by contour $A$. This says
that for failure~mode $C$ to occur failure mode $A$
must have occurred.
A famous example of this is the space shuttle `O' ring failure that
caused the 1986 Challenger disaster\cite{wdycwopt}.
For the failure mode to occur, the ambient temperature had to
be below a critical value.
If we take the failure mode of the `O' ring to be $C$
and the temperature below critical to be $A$, we can see that
the low temperature failure~mode $C$ can only occur if $A$ is true.
The `O' ring could fail in a different way independent of the critical temperature and this is 
represented, for the sake of this example, by contour $D$.

In terms of propositional logic, the inhibit gate of FTA\cite{nasafta}[pp 41-42], and the contour enclosure
of PLD represent {\em implication}.
\\
% \tiny
\begin{table}
%\vspace{0.3cm}
\centering
 \begin{tabular}{||c|c|c|c||} \hline \hline
   {\em $c$ }  & {\em $a$ } &  {\em $R1$  }      \\ \hline
       F         &  F  &    T     \\ \hline
       F         &  T  &    T     \\ \hline
       T         &  F  &    F     \\ \hline
       T         &  T  &    T     \\ \hline \hline
 \end{tabular}
%\vspace{0.3cm}
% \normalsize
\caption{Truth Table for diagram \ref{fig:inhibit}}
\end{table}

$$ R1 = c \implies a $$
$$ R2 = a $$
$$ R3 = d $$


\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, $R2$ is the symptom of either failure~mode $A$ or $C$
occurring. $R1$ is the symptom of $B$ or $A \wedge C$ occurring.
Note that although $R2$ is a symptom of the functional~group, on its own
it will not lead to a dangerous failure~mode of the subsystem.


% \subsection { Representing Logical Negation }
% 
% \begin{figure}[h+]
% %\centering
% %\input{ldor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldneg.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.60]{ldneg.eps}
% \caption{Logical Negation}
% \label{fig:ld_neg}
% \end{figure} % OR
% 
% Diagram \ref{fig:ld_neg} represents the logical equation $$ P = a \wedge b \wedge \neg c $$.
% 
% \paragraph{How this would be interpreted in failure analysis} 
% In failure analysis this test case represents the scenario where failure modes $a$ and $b$
% are active but $c$ is not.
% 
% 
% 
% \clearpage
% \subsection { Logical XOR example }
% 
% An exclusive or condition is represented by diagram \ref{fig:ld_xor}.
% The Equations represented are as follows.
% 
% firstly looking at the test case points
% $$ P = (\neg a \wedge b) $$ 
% $$ Q = (\neg b \wedge a) $$ 
% 
% now joining them with the disjuctive line
% $$ R = P \vee Q $$ 
% 
% Giving R as a Boolean equation
% $$ R = (\neg a \wedge b) \vee (\neg b \wedge a) $$
% or taking the symbol $\oplus$ to mean exclusive-or
% $$R = a \oplus b $$
% 
% 
% % \begin{figure}[h] %% SOMETHING IS WRONG says latex. very helpful tell me what it fucking is then
% % \centering
% % \caption{Example `XOR' Diagram}
% % \includegraphics[scale=0.80]{ldxor.eps}
% % \label{fig:ld_xor}
% % \end{figure} % XOR
% 
% 
% \begin{figure}[h+]
% %\centering
% %\input{millivolt_sensor.tex}
% \begin{center}
% % bb= llx lly urx ury; 
%  \includegraphics[width=200pt,bb=0pt 0pt 800pt 800pt]{logic_diagram/ldxor.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% 
% %\includegraphics[scale=0.4]{ldxor.eps}
% \caption{Logical XOR}
% \label{fig:ld_xor}
% \end{figure}
% 
% \clearpage
% \subsection { Logical IMPLICATION example }
% 
% 
% An implication $a \rightarrow b$ is represented by diagram \ref{fig:ld_imp}.
% The Equations represented are as follows.
% 
% Looking at the conjuctive environment of the test cases
% $$P = (\neg a)$$
% $$Q = (b)$$
% From the joining `disjunctive' line R in the diagram.
% $$R = P \vee Q$$
% Leading to
% $$R = (\neg a) \vee (b)$$
% which is the standard logic equation for implication.
% 
% \begin{figure}[h+]
% %\centering
% %\input{millivolt_sensor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldimp.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.4]{ldimp.eps}
% \caption{Logical Implication}
% \label{fig:ld_imp}
% \end{figure}
% 
% \tiny
% %\vspace{0.3cm}
% \begin{tabular}{||c|c|c|c||} \hline \hline
% 
%   {\em $a$ }  & {\em $b$ } &  {implication \em $(\neg a) \vee (b) $  }      \\ \hline
%       F         &  F  &    T     \\ \hline
%       F         &  T  &    T     \\ \hline
%       T         &  F  &    F     \\ \hline
%       T         &  T  &    T     \\ \hline \hline:
% \end{tabular}
% %\vspace{0.3cm}
% \normalsize
% 
% \clearpage
% \subsection { Diagram representing several Logic Equations Example }
% 
% 
% bb=0 0 450 404
% 
% 
% \begin{figure}[h+]
% %\centering
% %\input{millivolt_sensor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{logic_diagram/ldmeq.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.4]{ldmeq.eps}
% \caption{Several Logical Expressions}
% \label{fig:ld_meq}
% \end{figure}
% 
% %The effect of using explicit negation, means that a test case being outside a given contour does not imply negation, it implies a `don't care'
% %condition.
% 
% Three simple equations are represented in the  diagram \ref{fig:ld_dc}.
% 
% %The Set of contours $\mho$ represent the `don't care' conditions.
% 
% The Equations represented are as follows.
% 
% %$$ Q = a \; | \; \mho\{b,c\} $$
% 
% %$$ P = b \wedge c \; | \; \mho\{a\} $$
% 
% $$ Q = a $$
% $$ P = b \wedge c $$
% $$ R = b \vee c $$
% 
% % XXXXXX gives annoying impossible to understand syntax messages
% %\small
% %\bibliography{vmgbibliography,mybib}
% %\bibliography{vmgbibliography}
% %\normalsize
% 
\section{Intended use in FMMD}

The intention for these diagrams is that they are used to collect
component faults and combinations thereof, into faults that,
at the module level have the same symptoms.

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
which could inadvertently be placed into more than one $SMG$.
\ifthenelse {\boolean{paper}}
{
% explain unitary state failure modes here? I'd rather not have to in the `paper' version.... 16MAR2011
}
{
Having $SMG$s share test~cases would violate the concept of unitary state
failure modes (see \ref{sec:unitarystate}).
}

Syntax checking (looking for contradictions and tautologies), as well as detecting
errors of omission are automated in the FMMD tool.


\section{Double Simultaneous Fault Modelling}


Some deterministic based safety standards are specifying
that not only single component failure modes must be considered in 
analysis, but that the possibility of two component failing
simultaneously must be considered.
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 equipment under control (the burner) into a dangerous state.
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.
In practise, this would be a gigantic (as probably impossible task).
What we can consider though, are all faults being double simultaneous in the FMMD
methodology, because we need only look for the double failure modes within each functional group.
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}
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}.
Note that we have here all the single and double failure test cases in one diagram.
Also that all the contours intersect but do not enclose other contours: this
configuration is being termed \textbf{pair-wise intersection} of contours, in this study.

\begin{figure}[h]
 \centering
 \includegraphics[width=450pt,bb=0 0 677 527,keepaspectratio=true]{logic_diagram/doublesim.jpg}
 % doublesim.jpg: 677x527 pixel, 72dpi, 23.88x18.59 cm, bb=0 0 677 527
 \caption{Double and Single fault modes for a Functional Group with 3 failure modes}
 \label{fig:doublesim}
\end{figure}

\paragraph{Automated checking of double failure mode conditions.}
A PLD editor can be set to ensure that each diagram has a test case for every 
double simultaneous failure instance.

\pagebreak[3]
\section{N Simultaneous Errors}

There are systems where it may be necessary to model for N simultaneous failures.
This can be achieved in a PLD diagram by enclosing a test case with
all the failure modes to be modelled simultaneously, see figure \ref{fig:allfour}.

For instance, a 747 Aircraft with four engines, could suffer from
volcanic ash intake, affecting all engines.
Obviously the symptom of this multiple failure would be loss of propulsion and more importantly
the loss of ability to maintain altitude.
% and maybe even the APU !
The test case AFE represents the condition where all four engines have failed \cite{allfour}.
\begin{figure}[h]
 \centering
 \includegraphics[width=300pt,bb=0 0 349 236,keepaspectratio=true]{logic_diagram/allfourengines.jpg}
 % allfourengines.jpg: 349x236 pixel, 72dpi, 12.31x8.33 cm, bb=0 0 349 236
 \caption{PLD diagram showing a test~case where four fault modes are active}
 \label{fig:allfour}
\end{figure}

%\subsection{Example Sub-system}
%
%For instance were a `power supply' being analysed there could be several
%individual component faults or combinations that lead to
%a situation where there is no power. This can be described as a state 
%of the powersupply being modeelled as NO\_POWER.
%These can all be collected by  DISJUCNTION, i.e. that this this or this
%fault occuring will cause the NO\_POWER fault. Visually this disjuction is
%indicated by the joining lines.
%As far as the user of the `power supply' is concerned, the power supply has failed
%with the failure mode $NO\_POWER$.
%The `power supply' module, after this process will have a defined set of
%fault modes and may be considered as a component at a higher
%level of abstraction. This module can then be combined 
%with others at the same abstraction level.
%Note that because this is a fault collection process 
%the number of component faults for a module
%must be less than or equal to the sum of the number of component faults.

%Typeset in \ \ {\huge \LaTeX} \ \ on \ \  \today 

%\begin{verbatim}
%CVS Revision Identity $Id: logic_diagram.tex,v 1.17 2010/01/06 13:41:32 robin Exp $
%\end{verbatim}
%\ifthenelse {\boolean{paper}}
%{
%	\bibliographystyle{plain}
%        \bibliography{../vmgbibliography,../mybib}
%
%}
%{
%}
%Compiled last \today
%\end{document}

%\theend


%\pagebreak[4]
\clearpage