POST CONDITIONS
This commit is contained in:
parent
7746317e42
commit
08fad4c2f9
@ -136,6 +136,20 @@ be executed.
|
|||||||
%
|
%
|
||||||
In implementation code, a pre-condition violation should cause
|
In implementation code, a pre-condition violation should cause
|
||||||
an error to be generated, and thus a post condition to fail.
|
an error to be generated, and thus a post condition to fail.
|
||||||
|
%
|
||||||
|
A function can fail for reasons other than the
|
||||||
|
a failure of one the variables/inputs or functions that it calls.
|
||||||
|
Variables can become corrupted, by radiation affecting RAM or
|
||||||
|
by another software function erroneously overwriting variables.
|
||||||
|
Current work on software FMEA generally focuses on mapping
|
||||||
|
variable corruption to failure modes~\cite{procsfmea,procsfmeadb,sfmeaauto,sfmea}.
|
||||||
|
However, errors other than variable corruption can occur,
|
||||||
|
for instance a microprocessor may have subtle bugs in its instruction set or
|
||||||
|
incorrectly handled
|
||||||
|
interrupt contention could cause side effects in software.
|
||||||
|
For the failure mode model of any software function
|
||||||
|
we must consider all failure modes of post condition
|
||||||
|
violations as well as those caused by `components'.
|
||||||
|
|
||||||
|
|
||||||
\paragraph{Mapping contract `invariant' violations to symptoms and failure modes.}
|
\paragraph{Mapping contract `invariant' violations to symptoms and failure modes.}
|
||||||
@ -419,6 +433,7 @@ With these failure modes, we can analyse our first functional group, see table~\
|
|||||||
|
|
||||||
5: $ADC_{LOW}$ & output low & $LOW$ \\
|
5: $ADC_{LOW}$ & output low & $LOW$ \\
|
||||||
6: $ADC_{HIGH}$ & output high & $HIGH$ \\ \hline
|
6: $ADC_{HIGH}$ & output high & $HIGH$ \\ \hline
|
||||||
|
7: post condition fails & software fails & $V\_ERR$ \\ \hline
|
||||||
|
|
||||||
|
|
||||||
\hline
|
\hline
|
||||||
@ -509,6 +524,8 @@ We now analyse this hardware/software combined {\fg}.
|
|||||||
|
|
||||||
5: $CMATV_{LOW}$ & output low & $LOW$ \\ \hline
|
5: $CMATV_{LOW}$ & output low & $LOW$ \\ \hline
|
||||||
|
|
||||||
|
6: post condition fails & software fails & $VV\_ERR$ \\ \hline
|
||||||
|
|
||||||
\hline
|
\hline
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user