928 lines
34 KiB
TeX
928 lines
34 KiB
TeX
|
|
\ifthenelse {\boolean{paper}}
|
|
{
|
|
\begin{abstract}
|
|
%This chapter describes using diagrams to represent propositional logic.
|
|
Propositial 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
|
|
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 disiplines.
|
|
%
|
|
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{takeup}.
|
|
%
|
|
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}
|
|
Propositial 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
|
|
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 disiplines.
|
|
%
|
|
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 simplfy 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 provides a visual method for modelling failure~mode analysis
|
|
within these systems, and aids 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 percieved 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. 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.
|
|
%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 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 on the plane indicating a logical condition.
|
|
\item Conjunction - Overlapping contours
|
|
\item 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 points'.
|
|
The `test points' may be joined by joining lines.
|
|
A group of `test points' connected by joining lines
|
|
is defined as a `test point disjunction' or Spider.
|
|
Spiders may be labeled.
|
|
|
|
%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 points and joining lines that connect test points.
|
|
{
|
|
\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
|
|
a set of test point 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 countours.
|
|
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 points'.
|
|
% 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
|
|
% mandatory. How to describe ?????
|
|
Each test point 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 testpoint with a set of contours in the plane. This corresponds to the interior of the contours defining the zone.
|
|
}
|
|
}
|
|
|
|
Pairs of test points 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 points. 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 \} $$
|
|
}
|
|
}
|
|
|
|
%In English:
|
|
Test points on the concrete diagram pair-wise connected by a `joining line'
|
|
|
|
|
|
A collection of test points 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}.
|
|
An $SMG$ has members which are test points.
|
|
|
|
{
|
|
\definition{
|
|
%A spider is a set of test points where,
|
|
%a test point 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.
|
|
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.
|
|
|
|
}
|
|
}
|
|
|
|
A singleton test point can be considered a sequence of one test point 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 points $T$ (which
|
|
% are defined by the zone they inhabit) and pair wise connections $W$, which connect test points.
|
|
% Collections of test points, linked by shared conecting lines, form a set of test point groups $G$.
|
|
%
|
|
% A Zone defined by the contours that enclose it in the concrete diagram.
|
|
%
|
|
% $$ Z \subseteq C $$
|
|
%
|
|
% A test point $t \in T$ in habits a zone on the diagram.
|
|
%
|
|
% $$ \eta(t) = Z $$
|
|
%
|
|
% A joining line $$ w \in W $$ joins test points.
|
|
%
|
|
% $$ 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.
|
|
|
|
|
|
\subsection{Semantics of PLD}
|
|
|
|
\begin{itemize}
|
|
\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 $SMG$ represents the disjunction of all test points 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 disjunctively appended to it.
|
|
%
|
|
Let conjunctive logic equation associated with a test point
|
|
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 point 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.
|
|
|
|
$$ \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}} c $$
|
|
}
|
|
}
|
|
|
|
|
|
|
|
In English:
|
|
Thus a `test point' enclosed by contours labelled $a,b,c$ would be represented by the logic equation
|
|
$ a \wedge b \wedge c $.
|
|
|
|
{
|
|
\definition{
|
|
Let $\mathcal{G}_{fmg}$ 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
|
|
% $t$ is a `test point'
|
|
|
|
$$ \mathcal{G}:SMG \rightarrow P_{fmg} $$
|
|
|
|
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) \;) $$
|
|
}
|
|
}
|
|
|
|
The abstract PLD diagram is a set of logic equations representing all SMGs,
|
|
along with unused zones (i.e. zones that are not inhabited by SMGs).
|
|
{
|
|
\definition{
|
|
\label{SMGderivation}
|
|
A diagram can be reduced to a collection of $SMG$s.
|
|
A new diagram can be derived from this, replacing a contour for each SMG.
|
|
This diagram is at one higher level of abstraction then the diagram that
|
|
it was produced from.
|
|
}
|
|
}
|
|
|
|
|
|
\section{Example Diagrams}
|
|
|
|
|
|
\subsection {How to read a PLD diagram}
|
|
|
|
PLD diagrams are read by first looking at the test case points.
|
|
The test case asterisk will be enclosed by one or more contours.
|
|
These contours are collected and 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 dis-junction 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[bb=0 0 279 247]{logic_diagram/ldand.jpg}
|
|
% ldand.jpg: 279x247 pixel, 72dpi, 9.84x8.71 cm, bb=0 0 279 247
|
|
\label{fig:ld_and}
|
|
\end{figure}
|
|
|
|
% \begin{figure}[h+]
|
|
% \begin{center}
|
|
% \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldand.jpg}
|
|
% % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
|
% \end{center}
|
|
%
|
|
% %\includegraphics[scale=0.6]{ldand.eps}
|
|
% \caption{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 disjunctive joining lines and so this diagram represents one equation only, $ P = (a \wedge b) $.
|
|
Note that $P$ is considered to be 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.
|
|
|
|
\clearpage
|
|
\subsection { Logical XOR example }
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[bb=0 0 476 264]{logic_diagram/ldor.jpg}
|
|
% ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
|
|
\label{fig:ld_or}
|
|
\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 Boolean logic by first looking at the test cases, and
|
|
the contours they are placed on.
|
|
$$ 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 Boolean logic equations gives
|
|
\begin{equation}
|
|
\label{eqn:l_or}
|
|
R = ((a) \oplus (b))
|
|
\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 useage}
|
|
|
|
%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_meq}
|
|
shows three Functionally Merged groups, 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[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}
|
|
\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}
|
|
|
|
|
|
\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 can fail.
|
|
|
|
% \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
|
|
|
|
\clearpage
|
|
|
|
|
|
|
|
\subsection { Repeated Contour example }
|
|
|
|
|
|
Repeated contours are allowed in PLD diagrams.
|
|
Logical contradictions or tautologies can be detected automatically by
|
|
a software tool which assists in drawing these diagrams.
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=400pt,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 can appear more than once 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:repeat} is converted to Boolean logic by first looking at the test cases, and
|
|
the contours they are placed on.
|
|
$$ 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 residing in the intersection of contours $B$ 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 in $a \wedge b$.
|
|
This diagram is incomplete, there is no test case for the fault mode $a$.
|
|
The `available region' $a \backslash b$ has no test case, and this would be considered a `syntax error'
|
|
by the FMMD software tool.
|
|
|
|
|
|
|
|
\clearpage
|
|
|
|
|
|
\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 separate environmental condition.
|
|
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.\cite{nasafta}[pp41-42],\cite{nucfta}
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[bb=0 0 364 227]{logic_diagram/inhibit.jpg}
|
|
% inhibit.jpg: 404x252 pixel, 80dpi, 12.83x8.00 cm, bb=0 0 364 227
|
|
\label{fig:inhibit}
|
|
\end{figure}
|
|
%
|
|
% \begin{figure}[h]
|
|
% \centering
|
|
% \includegraphics[bb=0 0 364 228]{./inhibit.jpg}
|
|
% % inhibit.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 364 228
|
|
% \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 FTAi\cite{nasafta}[pp 41-42], and the contour enclosure
|
|
of PLD represent {\em implication}.
|
|
\\
|
|
% \tiny
|
|
\vspace{0.3cm}
|
|
\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
|
|
|
|
$$ 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 as intuitive.
|
|
Syntax checking (looking for contradictions and tautologies), as well as detecting
|
|
errors of ommission 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.
|
|
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 equipement 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.
|
|
\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 not that the contours intersect but do not enclose. This
|
|
configuration is being termed \textbf{pure instersection} of contours, in this study.
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=400pt,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.
|
|
|
|
\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.
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=400pt,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 testcase 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
|
|
|
|
|
|
|