diff --git a/logic_diagram/logic_diagram.tex b/logic_diagram/logic_diagram.tex index 5f88a89..9d56651 100644 --- a/logic_diagram/logic_diagram.tex +++ b/logic_diagram/logic_diagram.tex @@ -33,7 +33,7 @@ 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 +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} } @@ -92,12 +92,12 @@ for the analysis of safety critical software and hardware systems. Propositional Logic Diagrams (PLDs) have been created to collect and simplify fault~modes in safety critical systems undergoing -static analysis.%\cite{sccs}\cite{en61508}. +static analysis. %\cite{sccs}\cite{en61508}. % This type of analysis treats failure modes within a system as logical states. -PLD provides a visual method for modelling failure~mode analysis -within these systems, and aids the collection of +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 @@ -350,14 +350,14 @@ i.e. the contours $\mathcal{X}$ from the zone it inhabits. { \definition{ -Let $\mathcal{F}$ be a function mapping a test case $t \in T$, to a proposition / logical equation $p \in P$. +Let $\mathcal{F_t}$ be a function mapping a test case $t \in T$, to a proposition / logical equation $p \in P$. The test case $t$, inhabits the zone $\mathcal{Z}$ which is a collection of contours (the contours that enclose the test case). We can express this as -$$ \mathcal{F}:T \rightarrow P\;, $$ +$$ \mathcal{F_t}:T \rightarrow P\;, $$ %$$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} \Lambda c $$ given by -$$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} c \;. $$ +$$ \mathcal{F_t}(t): p = \bigwedge_{c \in \mathcal{Z}} c \;. $$ } } @@ -370,14 +370,15 @@ $ a \wedge b \wedge c $. { \definition{ Let $\mathcal{G}$ be a function that returns a logic equation for a given $SMG$ -$fmg$ in the diagram, where an SMG is a non empty set of test cases +$fmg$ in the diagram, where an SMG is a non empty set of test cases. % $t$ is a `test case' +$\mathcal{G}$ has a domain of SMG and a range of $P$ given as as -$$ \mathcal{G}:SMG \rightarrow P_{fmg}. $$ +$$ \mathcal{G}:SMG \rightarrow P. $$ -The logic equation (using $oplus$ to represent exclusive-or) representing an SMG $p_{fmg}$ can be determined thus; +The logic equation (using $oplus$ to represent exclusive-or) representing an SMG $p_{fmg}$ is given thus; -$$\mathcal{G}_{fmg}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F}_{t} (t) \;) \; .$$ +$$\mathcal{G}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F_t}_{t} (t) \;) \; .$$ } } @@ -385,8 +386,12 @@ The semantics of the diagram is the set of logic equations representing all its along with unused zones (i.e. zones that are not inhabited by SMGs). 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} +\include{../shortfg} \subsection{Symptom Collection} @@ -404,13 +409,21 @@ each SMG is represented by a contour. { \definition{ \label{SMGderivation} -A diagram can be drawn to represent the collection of $SMG$s. +%A diagram can be drawn to represent the collection of $SMG$s. +The diagram $d$ represents $SMG$s as graphs of asterisks connected with joining lines. A new diagram can be derived from this, replacing each SMG with a contour in the new diagram. 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$. } } +\subsection{Derived Component} +The diagram $d$ represents the failure modes of a functional group, +with the joining lines defining the its symptom collection. +The `symptom collection' respresents the functional group +at a higher level of failure mode abstraction. It represents the +{\fg} as a higher level component, or {\textbf{derived component}}, with a defined set of failure modes. \section{Example Diagrams} @@ -424,7 +437,7 @@ it was produced from. 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 form the logical conjunction +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; @@ -637,12 +650,12 @@ a software tool which assists in drawing these diagrams. The diagram \ref{fig:repeated} is converted to propositional logic by first looking at the test cases, and the contours they are placed on thus: -$$ P = (b) $$ +$$ 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 = P \oplus Q \;,$$ $$ R1 = b \oplus ( a \wedge c ) \; .$$ $R2$ joins two other test cases @@ -885,7 +898,8 @@ The intention for these diagrams is that they are used to collect component faults and combinations thereof, into faults that, at the module level have the same symptoms. -The act of collecting common symptoms by joining lines is seen as intuitive. % seen as BY ME ! HA ! +The act of collecting common symptoms by joining lines is seen more intuitive +than lists of logic equations. % seen as BY ME ! HA ! It also neatly by-passes the problem of having test cases which could inadvertently be placed into more than one $SMG$. Syntax checking (looking for contradictions and tautologies), as well as detecting