mirror of
https://github.com/smyalygames/checklist-tester.git
synced 2025-05-18 22:44:11 +02:00
feat(dissertation): add formal model design decision
This commit is contained in:
parent
4f588236ac
commit
8e4c9200a4
@ -5,7 +5,7 @@
|
|||||||
\begin{figure}[!h]
|
\begin{figure}[!h]
|
||||||
\centering
|
\centering
|
||||||
\begin{tikzpicture} [align=center, node distance=4cm]
|
\begin{tikzpicture} [align=center, node distance=4cm]
|
||||||
\node (connector) [box] {Checklist Tester Initerface};
|
\node (connector) [box] {Checklist Tester Interface};
|
||||||
\node (server) [box, below of=connector] {Checklist Tester Server};
|
\node (server) [box, below of=connector] {Checklist Tester Server};
|
||||||
\node (plugin) [box, right of=server] {Simulator Connector Plugin};
|
\node (plugin) [box, right of=server] {Simulator Connector Plugin};
|
||||||
\node (formal) [box, left of=server] {Formal Method};
|
\node (formal) [box, left of=server] {Formal Method};
|
||||||
@ -49,4 +49,31 @@
|
|||||||
look out for
|
look out for
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
|
|
||||||
|
\section{Decisions}
|
||||||
|
\begin{itemize}
|
||||||
|
\item There would be around 3 main components to this tester
|
||||||
|
\begin{itemize}
|
||||||
|
\item Formal Model
|
||||||
|
\item Flight Simulator plugin
|
||||||
|
\item Checklist Tester (to connect the formal model and flight simulator)
|
||||||
|
\end{itemize}
|
||||||
|
\item As VDM-SL is being used, it uses VDMJ to parse the model~\cite{vdmj}. This was a starting
|
||||||
|
point for the tech stack, as VDMJ is also open source.
|
||||||
|
\item VDMJ uses Java, therefore my language of choice was a language related to Java.
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
\subsection{Formal Model}
|
||||||
|
\begin{itemize}
|
||||||
|
\item There were a few ways of implementing the formal model into another application
|
||||||
|
\item Some of these methods were provided by Overture~\cite{overture-remote}
|
||||||
|
\begin{itemize}
|
||||||
|
\item RemoteControl interface
|
||||||
|
\item VDMTools API~\cite{vdmtoolbox-api}
|
||||||
|
\end{itemize}
|
||||||
|
\item However, both of these methods did not suit what was required as most of the
|
||||||
|
documentation for RemoteControl was designed for the Overture Tool IDE. VDMTools
|
||||||
|
may have handled the formal model differently
|
||||||
|
\item The choice was to create a VDMJ wrapper, as the modules are available on Maven
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
\end{document}
|
\end{document}
|
||||||
|
Binary file not shown.
@ -82,3 +82,35 @@
|
|||||||
urldate = {2024-02-23},
|
urldate = {2024-02-23},
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@online{vdmj,
|
||||||
|
author = {Nick Battle},
|
||||||
|
title = {VDMJ},
|
||||||
|
url = {https://github.com/nickbattle/vdmj},
|
||||||
|
urldate = {2024-04-21},
|
||||||
|
}
|
||||||
|
|
||||||
|
@manual{overture-remote,
|
||||||
|
author = {Peter Gorm Larsen and Kenneth Lausdahl and Peter Jørgensen and Joey
|
||||||
|
Coleman and Sune Wolff and Nick Battle},
|
||||||
|
title = {Overture VDM-10 Tool Support: User Guide},
|
||||||
|
institution = {The Overture Initiative},
|
||||||
|
url = {
|
||||||
|
https://raw.github.com/overturetool/documentation/editing/documentation/UserGuideOvertureIDE/OvertureIDEUserGuide.pdf
|
||||||
|
},
|
||||||
|
chapter = {16},
|
||||||
|
pages = {81-98},
|
||||||
|
number = {TR-2010-02},
|
||||||
|
year = {2013},
|
||||||
|
month = {04},
|
||||||
|
}
|
||||||
|
|
||||||
|
@manual{vdmtoolbox-api,
|
||||||
|
author = {Kyushu University},
|
||||||
|
title = {The VDM Toolbox API},
|
||||||
|
url = {
|
||||||
|
https://github.com/vdmtools/vdmtools/raw/stable/doc/api-man/ApiMan_a4E.pdf
|
||||||
|
},
|
||||||
|
version = {1.0},
|
||||||
|
year = {2016},
|
||||||
|
}
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user