Friday afternoon edits. Getting ready for 3 core chapters for 20AUG2010
This commit is contained in:
parent
3a4642a8dc
commit
c1b01133ba
@ -295,7 +295,7 @@ A set of failure modes where only one fault mode
|
|||||||
can be active at a time is termed a `unitary~state' failure mode set.
|
can be active at a time is termed a `unitary~state' failure mode set.
|
||||||
%This is termed the $U$ set thoughout this study.
|
%This is termed the $U$ set thoughout this study.
|
||||||
This corresponds to the `mutually exclusive' definition in
|
This corresponds to the `mutually exclusive' definition in
|
||||||
probability theory\cite{probandstat}.
|
probability theory\cite{probstat}.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
Let the set of all possible components to be $\mathcal{C}$
|
Let the set of all possible components to be $\mathcal{C}$
|
||||||
@ -370,7 +370,7 @@ we have banned larger combinations as well.
|
|||||||
For some integrity levels of static analysis there is a need to consider not only single
|
For some integrity levels of static analysis there is a need to consider not only single
|
||||||
failure modes in isolation, but cases where more then one failure mode may occur
|
failure modes in isolation, but cases where more then one failure mode may occur
|
||||||
simultaneously.
|
simultaneously.
|
||||||
It is an implied requirement of EN298 for instance to consider double simultaneous faults.
|
It is an implied requirement of EN298\cite{en298} for instance to consider double simultaneous faults.
|
||||||
To generalise, we may need to consider $N$ simultaneous
|
To generalise, we may need to consider $N$ simultaneous
|
||||||
failure modes when analysing a functional group. This involves finding
|
failure modes when analysing a functional group. This involves finding
|
||||||
all combinations of failures modes of size $N$ and less.
|
all combinations of failures modes of size $N$ and less.
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
|
|
||||||
\section{Introduction}
|
\section{Introduction}
|
||||||
|
|
||||||
$$ \int_{0\-}^{\infty} f(t).e^{-s.t}.dt \; | \; s \in \mathcal{C}$$
|
%% $$ \int_{0\-}^{\infty} f(t).e^{-s.t}.dt \; | \; s \in \mathcal{C}$$
|
||||||
|
|
||||||
This thesis describes the application of, mathematical (formal) techniques to
|
This thesis describes the application of, mathematical (formal) techniques to
|
||||||
the design of safety critical systems.
|
the design of safety critical systems.
|
||||||
@ -30,19 +30,19 @@ They are generally left running unattended for long periods.
|
|||||||
They are subject to stringent safety regulations and
|
They are subject to stringent safety regulations and
|
||||||
must conform to specific `EN' standards.
|
must conform to specific `EN' standards.
|
||||||
|
|
||||||
One cannot merely comply with the standards.
|
For a non-safety critical product one can merely comply with the standards, and `self~certify' by applying a CE mark sticker.
|
||||||
|
Safety critical products are categorised and listed. These require
|
||||||
The product must be `certified' by an independent
|
certification by an independent and `competent body' recognised under European law.
|
||||||
and
|
The certification process typically involves stress testing with repeated operation cycles
|
||||||
`competent body' recognised under European law.
|
over a specified a range of temperatures, electrical stress testing with high voltage interference,
|
||||||
The certification involved stress testing with repeated operation cycles,
|
power supply voltage ranges with surges and dips, electro static discharge testing, and
|
||||||
over a specified a range of temperatures, electrical stress testing with high voltage interference, and
|
|
||||||
power supply voltage surges and dips, electro static discharge testing, and
|
|
||||||
EMC (Electro Magnetic Compatibility). A significant part
|
EMC (Electro Magnetic Compatibility). A significant part
|
||||||
of this process however, was `static testing'. This involved looking at the design of the products,
|
of this process however, is `static testing'. This involves looking at the design of the products,
|
||||||
from the perspective of components failing, and the effect on safety this would have.
|
from the perspective of environmental stresses, natural input fault conditions\footnote{For instance in a burner controller, the gas supply pressure reducing},
|
||||||
Some of the static testing involved checking that the germane `EN' standards had
|
components failing, and the effects on safety this could have.
|
||||||
been complied with. Failure Mode Effects Analysis (FMEA) was also applied. This involved
|
Some static testing involves checking that the germane `EN' standards have
|
||||||
|
been complied with\footnore{for instance protection levels of enclosure, or down rating of electrical components}.
|
||||||
|
Failure Mode Effects Analysis (FMEA) was also applied. This involved
|
||||||
looking in detail at selected critical sections of the product and proposing
|
looking in detail at selected critical sections of the product and proposing
|
||||||
component failure scenarios.
|
component failure scenarios.
|
||||||
For each failure scenario proposed either a satisfactory
|
For each failure scenario proposed either a satisfactory
|
||||||
@ -311,15 +311,15 @@ fault conditions are missed.
|
|||||||
|
|
||||||
% http://en.wikipedia.org/wiki/Autopilot
|
% http://en.wikipedia.org/wiki/Autopilot
|
||||||
\paragraph{Importance of self checking}
|
\paragraph{Importance of self checking}
|
||||||
To take an example of an Autopilot, simple early autopilots,
|
To take an example of an Aircraft Autopilot, simple early devices\footnote{from the 1920's simple aircraft autopilots were in service},
|
||||||
prevented the aircraft staying from a compass bearing and kept it flying striaght and level.
|
prevented the aircraft straying from a compass bearing and kept it flying straight and level.
|
||||||
Were they to fail the pilot would notice quite quickly
|
Were they to fail the pilot would notice quite quickly
|
||||||
and resume manual control of the bearing.
|
and resume manual control of the bearing.
|
||||||
|
|
||||||
Modern autopilots control all aspects of flight including the engines, take off and landing phases.
|
Modern autopilots control all aspects of flight including the engines, take off and landing phases.
|
||||||
The automated system does not have the
|
The automated system do not have the
|
||||||
common sense of a human pilot either and if fed the wrong sensory information
|
common sense of a human pilot; and if fed the incorrect sensory information
|
||||||
could make horrendous mistakes. This means that simply reading sensors and applying control
|
can make horrendous mistakes. This means that simply reading sensors and applying control
|
||||||
corrections cannot be enough.
|
corrections cannot be enough.
|
||||||
Checking for error conditions must also be incorporated.
|
Checking for error conditions must also be incorporated.
|
||||||
It could also develop an internal fault, and must be able to recognise and cope with this.
|
It could also develop an internal fault, and must be able to recognise and cope with this.
|
||||||
@ -345,7 +345,7 @@ It could also develop an internal fault, and must be able to recognise and cope
|
|||||||
|
|
||||||
|
|
||||||
\paragraph{Component added to detect errors}
|
\paragraph{Component added to detect errors}
|
||||||
The op-amp in the circuit in figure \ref{fig:imillivolt}, supplies a gain of $\approx 180$ \footnote{
|
The op-amp in the circuit in figure \ref{fig:millivolt}, supplies a gain of $\approx 180$ \footnote{
|
||||||
applying formula for non-inverting op-amp gain\cite{aoe} $\frac{150 \times 10^3}{820}+ 1 = 183$ }.
|
applying formula for non-inverting op-amp gain\cite{aoe} $\frac{150 \times 10^3}{820}+ 1 = 183$ }.
|
||||||
The safety case here is that
|
The safety case here is that
|
||||||
any amplified signal between 0.5 and 4 volts on the ADC will be considered in range.
|
any amplified signal between 0.5 and 4 volts on the ADC will be considered in range.
|
||||||
@ -355,7 +355,15 @@ are produced by the Seebeck effect\cite{aoe}}
|
|||||||
Should the sensor become disconnected the input will drift up due to the safety resistor $R18$.
|
Should the sensor become disconnected the input will drift up due to the safety resistor $R18$.
|
||||||
This will cause the opamp to supply its maximum voltage, telling the system the sensor reading is invalid.
|
This will cause the opamp to supply its maximum voltage, telling the system the sensor reading is invalid.
|
||||||
Should the sensor become shorted, the input will fall below 3mV and the op amp will
|
Should the sensor become shorted, the input will fall below 3mV and the op amp will
|
||||||
supply a voltage below 0.5.
|
supply a voltage below 0.5. Note that the sensor breaking and becoming open, or
|
||||||
|
becoming disconnected is the `Raison d'être' of this safety addition.
|
||||||
|
This circuit would typically be used to amplify a thermocouple, which typically
|
||||||
|
fails by going open circuit.
|
||||||
|
It {\em does}
|
||||||
|
detect several other failure modes of this circuit and a full analysis is given in appendix \ref{mvamp}.
|
||||||
|
% Note C14 shorting is potentially v dangerous could lead to a high output by the opamp being seen as a
|
||||||
|
% low temperature.
|
||||||
|
|
||||||
%
|
%
|
||||||
\paragraph{Self Checking}
|
\paragraph{Self Checking}
|
||||||
This introduces a level of self checking into the system.
|
This introduces a level of self checking into the system.
|
||||||
@ -481,6 +489,12 @@ But because of the top down nature of the FTA technique, the safety designer mus
|
|||||||
the environemtnal constraints of all component parts in order to use this correctly.
|
the environemtnal constraints of all component parts in order to use this correctly.
|
||||||
This element of FTA is discussed in \ref{surveysc}
|
This element of FTA is discussed in \ref{surveysc}
|
||||||
|
|
||||||
|
\section{Therac 25}
|
||||||
|
|
||||||
|
%% Here need more detail of what therac 25 was and roughly how it failed
|
||||||
|
%% with refs to nancy
|
||||||
|
%% and then highlight the fact that the safety analysis did not integrate software and hardware domains.
|
||||||
|
|
||||||
\section{Problems with Natural Language}
|
\section{Problems with Natural Language}
|
||||||
|
|
||||||
Written natural language desciptions can not only be ambiguous or easy to misinterpret, it
|
Written natural language desciptions can not only be ambiguous or easy to misinterpret, it
|
||||||
@ -534,7 +548,7 @@ temperature being the most typical. Very often what happens to the system outsid
|
|||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item To create a Bottom up FMEA technique that permits a connected hierarchy to be
|
\item To create a Bottom up FMEA technique that permits a connected hierarchy to be
|
||||||
built representing the fault behaviour of a system.
|
built representing the fault behaviour of a system.
|
||||||
\item To create a procedure where no component failure mode can be un-handled.
|
\item To create a procedure where no component failure mode can be accidentally ignored.
|
||||||
\item To create a user friendly formal common visual notation to represent fault modes
|
\item To create a user friendly formal common visual notation to represent fault modes
|
||||||
in Software, Electronic and Mechanical sub-systems.
|
in Software, Electronic and Mechanical sub-systems.
|
||||||
\item To formally define this visual language in concrete and abstract domains.
|
\item To formally define this visual language in concrete and abstract domains.
|
||||||
@ -544,7 +558,7 @@ highest abstract system 'top level'.
|
|||||||
\item To formally define the hierarchies and procedure for bulding them.
|
\item To formally define the hierarchies and procedure for bulding them.
|
||||||
\item To produce a software tool to aid in the drawing of diagrams and
|
\item To produce a software tool to aid in the drawing of diagrams and
|
||||||
ensuring that all fault modes are addressed.
|
ensuring that all fault modes are addressed.
|
||||||
\item to provide for deterministic and probablistic failure mode analysis processes
|
\item to provide a data model that can be used as a source for deterministic and probablistic failure mode analysis reports.
|
||||||
\item To allow the possiblility of MTTF calculation for statistical
|
\item To allow the possiblility of MTTF calculation for statistical
|
||||||
reliability/safety calculations.
|
reliability/safety calculations.
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
|
@ -614,10 +614,14 @@ by the FMMD software tool.
|
|||||||
|
|
||||||
\subsection { Inhibit Failure }
|
\subsection { Inhibit Failure }
|
||||||
|
|
||||||
|
%
|
||||||
|
% very interesting here Inhibit is ENCLOSURE and simultaneous faults are PURE INTERSECTION
|
||||||
|
%
|
||||||
|
|
||||||
|
|
||||||
Very often a failure mode can only occur
|
Very often a failure mode can only occur
|
||||||
given a separate environmental condition.
|
given a separate environmental condition.
|
||||||
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.\cite{NASA},\cite{NUK}
|
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.\cite{FTA}[pp41-42],\cite{NUK}
|
||||||
|
|
||||||
\begin{figure}[h]
|
\begin{figure}[h]
|
||||||
\centering
|
\centering
|
||||||
@ -634,7 +638,7 @@ In Fault Tree Analysis (FTA) this is represented by an inhibit gate.\cite{NASA},
|
|||||||
% \end{figure}
|
% \end{figure}
|
||||||
|
|
||||||
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
||||||
Contour $C$ is enclosed by contour $A$. This says
|
Contour $C$ is \textbf{enclosed} by contour $A$. This says
|
||||||
that for failure~mode $C$ to occur failure mode $A$
|
that for failure~mode $C$ to occur failure mode $A$
|
||||||
must have occurred.
|
must have occurred.
|
||||||
A well known example of this is the space shuttle `O' ring failure that
|
A well known example of this is the space shuttle `O' ring failure that
|
||||||
@ -845,6 +849,8 @@ To cover this rigorously, we are bound to consider more than one fault being act
|
|||||||
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}.
|
||||||
Note that we have here all the single and double failure test cases in one diagram.
|
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]
|
\begin{figure}[h]
|
||||||
\centering
|
\centering
|
||||||
|
@ -89,6 +89,13 @@
|
|||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@BOOK{probstat,
|
||||||
|
AUTHOR = " M~R~Spiegel",
|
||||||
|
TITLE = "Probability and Statistics Second edition : SHCAUM'S : ISBN 0-07-135004-7",
|
||||||
|
PUBLISHER = "Oxford University Press",
|
||||||
|
YEAR = "1988"
|
||||||
|
}
|
||||||
|
|
||||||
@BOOK{idmfssz,
|
@BOOK{idmfssz,
|
||||||
AUTHOR = " D~C~Ince",
|
AUTHOR = " D~C~Ince",
|
||||||
TITLE = " An Introduction to Discrete Mathematics, Formal System Specification and Z : Oxford : ISBN 0-19-853836-7",
|
TITLE = " An Introduction to Discrete Mathematics, Formal System Specification and Z : Oxford : ISBN 0-19-853836-7",
|
||||||
|
@ -282,24 +282,34 @@ $$ FCS(R) = SP $$
|
|||||||
|
|
||||||
%\REQUIRE {All failure modes for the components in $fm_i = FM(fg_i)$}
|
%\REQUIRE {All failure modes for the components in $fm_i = FM(fg_i)$}
|
||||||
\STATE {Let $sp_l$ be a set of `test cases results' where $l$ is an index set $L$}
|
\STATE {Let $sp_l$ be a set of `test cases results' where $l$ is an index set $L$}
|
||||||
\STATE {Let $SP$ be a set whose members are sets $sp_l$}
|
\STATE {Let $SP$ be a set whose members are the indexed `symptoms' $sp_l$}
|
||||||
\COMMENT{ $SP$ is the set of `fault symptoms' for the sub-system}
|
\COMMENT{ $SP$ is the set of `fault symptoms' for the sub-system}
|
||||||
|
\STATE{$SP := 0$} \COMMENT{ initialise the `symptom family set'}
|
||||||
%
|
%
|
||||||
%\COMMENT{This corresponds to a fault symptom of the functional group $FG$}
|
%\COMMENT{This corresponds to a fault symptom of the functional group $FG$}
|
||||||
%\COMMENT{where double failure modes are required the cardinality constrained powerset of two must be applied to each failure mode}
|
%\COMMENT{where double failure modes are required the cardinality constrained powerset of two must be applied to each failure mode}
|
||||||
|
\REPEAT
|
||||||
|
|
||||||
\FORALL { $ r_j \in R$ }
|
\STATE{$sp_l := 0$} \COMMENT{ initialise the `symptom'}
|
||||||
\STATE { $sp_l \in \mathcal{P} R \wedge sp_l \in SP$ }
|
\STATE{$sp_l \in \mathcal{P} R$} \COMMENT{Select common symptoms from the results set}
|
||||||
%\STATE { $sp_l \in \bigcap R \wedge sp_l \in SP$ }
|
\STATE{$ R := R \backslash sp_l $} \COMMENT{remove the results used from the results set}
|
||||||
\COMMENT{ Collect common symptoms.
|
\STATE{$ SP := SP \cup sp_l$} \COMMENT{collect the symptom into the symtom family set SP}
|
||||||
Analyse the sub-system's fault behaviour under the failure modes in $tc_j$ and determine the symptoms $sp_l$ that it
|
\STATE{$ l := l + 1 $} \COMMENT{move the index up for the next symptom to collect}
|
||||||
causes in the functional group $FG$}
|
|
||||||
%\ENSURE { $ \forall l2 \in L ( \forall l1 \in L | \exists a \in sp_{l1} \neq \exists b \in sp_{l2} \wedge l1 \neq l2 ) $}
|
|
||||||
|
|
||||||
\ENSURE {$ \forall a \in sp_l \;such\;that\; \forall sp_i \in \bigcap_{i=1..L} SP ( sp_i = sp_l \implies a \in sp_i)$}
|
\UNTIL{ $ R = \emptyset $ } \COMMENT{continue until all results belong to a symptom}
|
||||||
\COMMENT { Ensure that the elements in each $sp_l$ are not present in any other $sp_l$ set }
|
|
||||||
|
|
||||||
\ENDFOR
|
%% \FORALL { $ r_j \in R$ }
|
||||||
|
%% \STATE { $sp_l \in \mathcal{P} R \wedge sp_l \in SP$ }
|
||||||
|
%% %\STATE { $sp_l \in \bigcap R \wedge sp_l \in SP$ }
|
||||||
|
%% \COMMENT{ Collect common symptoms.
|
||||||
|
%% Analyse the sub-system's fault behaviour under the failure modes in $tc_j$ and determine the symptoms $sp_l$ that it
|
||||||
|
%%causes in the functional group $FG$}
|
||||||
|
%% %\ENSURE { $ \forall l2 \in L ( \forall l1 \in L | \exists a \in sp_{l1} \neq \exists b \in sp_{l2} \wedge l1 \neq l2 ) $}
|
||||||
|
%%
|
||||||
|
%% \ENSURE {$ \forall a \in sp_l \;such\;that\; \forall sp_i \in \bigcap_{i=1..L} SP ( sp_i = sp_l \implies a \in sp_i)$}
|
||||||
|
%% \COMMENT { Ensure that the elements in each $sp_l$ are not present in any other $sp_l$ set }
|
||||||
|
%%
|
||||||
|
%% \ENDFOR
|
||||||
\STATE { The Set $SP$ can now be considered to be the set of fault modes for the sub-system that $FG$ represents}
|
\STATE { The Set $SP$ can now be considered to be the set of fault modes for the sub-system that $FG$ represents}
|
||||||
|
|
||||||
\RETURN $SP$
|
\RETURN $SP$
|
||||||
|
Loading…
Reference in New Issue
Block a user