mirror of
https://github.com/smyalygames/checklist-tester.git
synced 2025-11-30 01:39:38 +01:00
feat(dissertation): add formal methods section in background
This commit is contained in:
@@ -88,10 +88,21 @@
|
|||||||
% 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
|
||||||
|
|
||||||
\subsection{History}
|
\begin{itemize}
|
||||||
|
\item Formal methods is a mathematical technique that can be used towards the
|
||||||
|
verification of a system~\cite{nasa:formal}
|
||||||
\subsection{Application}
|
\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
|
||||||
|
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
|
||||||
|
verification process~\cite{airbus:formal}
|
||||||
|
\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
|
||||||
|
and analysis of the numerical precision and stability of floating-point operators
|
||||||
|
to name a few~\cite{airbus:formal}
|
||||||
|
\item There are a multitude of specification languages, each of them
|
||||||
|
having their own reasons % TODO don't know if this should be included
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
|
||||||
%%%%% SOLUTION STACK %%%%%
|
%%%%% SOLUTION STACK %%%%%
|
||||||
|
|||||||
Binary file not shown.
@@ -1 +1 @@
|
|||||||
4915
|
5035
|
||||||
|
|||||||
@@ -47,8 +47,27 @@
|
|||||||
url = {https://ntrs.nasa.gov/citations/20160013263},
|
url = {https://ntrs.nasa.gov/citations/20160013263},
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@online{nasa:formal,
|
||||||
|
author = {NASA Langley Formal Methods Research Program},
|
||||||
|
title = {Langley Formal Methods Program • What is Formal Methods},
|
||||||
|
url = {https://shemesh.larc.nasa.gov/fm/fm-what.html},
|
||||||
|
urldate = {2024-05-20}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{airbus:formal,
|
||||||
|
author={Laurent, Odile},
|
||||||
|
booktitle={2010 Third International Conference on Software Testing, Verification and Validation},
|
||||||
|
title={Using Formal Methods and Testability Concepts in the Avionics Systems Validation and Verification (V\&V) Process},
|
||||||
|
year={2010},
|
||||||
|
volume={},
|
||||||
|
number={},
|
||||||
|
pages={1-10},
|
||||||
|
keywords={System testing;Aerospace electronics;Automatic testing;Formal specifications;Aircraft;Software testing;Ground support;Assembly systems;Fault diagnosis;Automation;Formal methods;testing strategy;automatic test case generation;validation and verification},
|
||||||
|
doi={10.1109/ICST.2010.38}
|
||||||
|
}
|
||||||
|
|
||||||
@book{manifesto,
|
@book{manifesto,
|
||||||
author = {Atul Gawande},
|
author = {Gawande, Atul},
|
||||||
title = {The Checklist Manifesto: How To Get Things Right},
|
title = {The Checklist Manifesto: How To Get Things Right},
|
||||||
publisher = {Profile Books},
|
publisher = {Profile Books},
|
||||||
edition = {Main Edition},
|
edition = {Main Edition},
|
||||||
|
|||||||
Reference in New Issue
Block a user