robin/Robin_PHD
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

pre cond violation in s/w expanded on

Browse Source
This commit is contained in:
Robin Clark 2012-11-20 05:58:38 +00:00
parent 4baf8387cc
commit 06bd918d54
1 changed files with 15 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
submission_thesis/CH5_Examples/software.tex
View File

@ -87,6 +87,15 @@ A precondition, or requirement for a contract software function
defines the correct ranges of input conditions for the function defines the correct ranges of input conditions for the function
to operate successfully. to operate successfully.
% %
% C Garret said this was unclear so I have added the following two sentences.
%
If we consider a software function to be a {\fg} in the FMMD sense,
we see that it is can be considered to be a collection of functions that it
calls and variables/inputs that it uses.
%
If we consider these functions and inputs to be its components,
any erroneous behaviour from them can be considered to be a component failure mode.
%
For a software function, a violation of a pre-condition is For a software function, a violation of a pre-condition is
in effect a failure mode of `one of its components'. in effect a failure mode of `one of its components'.
@ -96,6 +105,12 @@ in effect a failure mode of `one of its components'.
A post condition is a definition of correct behaviour by a function. A post condition is a definition of correct behaviour by a function.
A violated post condition is a symptom of failure, or derived failure mode, of a function. A violated post condition is a symptom of failure, or derived failure mode, of a function.
Post conditions could be either actions performed (i.e. the state of hardware changed) or an output value of a function. Post conditions could be either actions performed (i.e. the state of hardware changed) or an output value of a function.
In pure contract programming, a violation of a pre-condition would not cause the function to
be executed.
%
In implementation code, a pre-condition violation should cause
an error to be generated, and thus a post condition to fail.
\paragraph{Mapping contract `invariant' violations to symptoms and failure modes.} \paragraph{Mapping contract `invariant' violations to symptoms and failure modes.}
@ -779,11 +794,6 @@ In this project we are using the ADCMUX, TIMER, PWM and the general purpose comp
We have to therefore consider the general~computing, CLOCK, PROM and RAM failure modes. We have to therefore consider the general~computing, CLOCK, PROM and RAM failure modes.
$$fm (micro-controller) =\{ PROM\_FAULT, RAM\_FAULT, CPU\_FAULT, ALU\_FAULT, CLOCK\_STOPPED \}.$$ $$fm (micro-controller) =\{ PROM\_FAULT, RAM\_FAULT, CPU\_FAULT, ALU\_FAULT, CLOCK\_STOPPED \}.$$
\subsection{Temperature Controller Software Elements FMMD} \subsection{Temperature Controller Software Elements FMMD}
We must start from the bottom-up with the software, and consider the hardware elements We must start from the bottom-up with the software, and consider the hardware elements
@ -793,20 +803,6 @@ Starting at the bottom
%\clearpage %\clearpage
\section{Conclusion: Software/Hardware FMMD Model} \section{Conclusion: Software/Hardware FMMD Model}