smyalygames/checklist-tester
1
0
Fork 0
mirror of https://github.com/smyalygames/checklist-tester.git synced 2025-05-18 14:34:12 +02:00
Code Issues Actions Packages Projects Releases Wiki Activity

feat(dissertation): write formal methods background in full

Browse Source
This commit is contained in:
Anthony Berg 2024-05-22 01:29:40 +01:00
parent 78096bba2a
commit 4a44ba7344
2 changed files with 28 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
pub/dissertation/chapters/background.tex
View File

@ -168,21 +168,34 @@ situations where the crew may completely ignore safety procedures and systems.
% TODO add quick overview of what Formal Methods are % TODO add quick overview of what Formal Methods are
% Potential resource: https://shemesh.larc.nasa.gov/fm/fm-what.html % Potential resource: https://shemesh.larc.nasa.gov/fm/fm-what.html
\begin{itemize} % \begin{itemize}
\item Formal methods is a mathematical technique that can be used towards the % \item Formal methods is a mathematical technique that can be used towards the
verification of a system~\cite{nasa:formal} % verification of a system~\cite{nasa:formal}
\item This can be used to verify correctness of all the inputs in a system~\cite{nasa:formal} % \item This can be used to verify correctness of all the inputs in a system~\cite{nasa:formal}
\item Hence, as dealing with safety, it would be beneficial to have % \item Hence, as dealing with safety, it would be beneficial to have
the logic of this testing tool verified, to avoid bugs and misleading results % the logic of this testing tool verified, to avoid bugs and misleading results
\item Airbus also uses formal methods in their avionics systems validation and % \item Airbus also uses formal methods in their avionics systems validation and
verification process~\cite{airbus:formal} % verification process~\cite{airbus:formal}
\item Some examples where Airbus used formal methods was during the development % \item Some examples where Airbus used formal methods was during the development
for the Airbus A380, where they used it for proof of absence of stack overflows % for the Airbus A380, where they used it for proof of absence of stack overflows
and analysis of the numerical precision and stability of floating-point operators % and analysis of the numerical precision and stability of floating-point operators
to name a few~\cite{airbus:formal} % to name a few~\cite{airbus:formal}
\item There are a multitude of specification languages, each of them % \item There are a multitude of specification languages, each of them
having their own reasons % TODO don't know if this should be included % having their own reasons % TODO don't know if this should be included
\end{itemize} % \end{itemize}
Formal methods is a mathematical technique that can be used towards the verification
of a system, that could either be a piece of software or hardware.
Therefore, this can be used to verify correctness of all the inputs in a system.~\cite{nasa:formal}
Hence, as this project is dealing with safety, it would be beneficial to use
formal methods for testing and verification.
An example of where formal methods is used within aviation is by Airbus, where
it was used during the development of the Airbus A380. Formal methods was used to test
the A380 for proof of absence of stack overflows and analysis of the numerical precision
and stability of floating-point operators to name a few.~\cite{airbus:formal}
% TODO maybe add a section about the amount of specification languages that exist?
%%%%% SOLUTION STACK %%%%% %%%%% SOLUTION STACK %%%%%

BIN
pub/dissertation/dissertation.pdf
View File

Binary file not shown.