\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage{amsmath, amssymb}
\usepackage[numbers]{natbib}
\bibliographystyle{abbrvnat}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\makeatletter
\g@addto@macro{\UrlBreaks}{\UrlOrds}
\makeatother

\begin{document}

\title{Verified Complete Test Strategies for Finite State Machines}
\author{Robert Sachtleben}
\maketitle

\begin{abstract}
	This entry provides executable formalisations of the following testing strategies based on finite state machines (FSM):
\begin{enumerate}
	\item Strategies for language-equivalence testing on possibly nondeterministic and partial FSMs:
	\begin{itemize}
		\item W-Method \cite{chow:wmethod} 
		\item Wp-Method (based on a generalisation of~\cite{luo_test_1994} presented in~\cite{PeleskaHuangLectureNotesMBT})
		\item HSI-Method \cite{luo_selecting_1995}
		\item H-Method \cite{DBLP:conf/forte/DorofeevaEY05}
		\item SPY-Method \cite{simao_reducing_2012}
		\item SPYH-Method \cite{Soucha2018}
	\end{itemize}
	\item Strategies for reduction testing on possibly nondeterministic FSMs:
	\begin{itemize}
		\item Adaptive state counting (as described in \cite{DBLP:conf/hase/PetrenkoY14})
	\end{itemize}
\end{enumerate}
	These strategies are implemented using generic frameworks which allow combining parts of strategies such as reaching and distinguishing of states or distributing traces over classes of convergent traces. Further details are given in the corresponding PhD thesis~\cite{elib_6068} and tools employing the code generated from this entry are available at \url{https://bitbucket.org/RobertSachtleben/an-approach-for-the-verification-and-synthesis-of-complete}.
	
	In addition to formalising different algorithms, this entry differs from my previous entry \cite{Adaptive_State_Counting-AFP} (see \cite{Sachtleben2019} for the corresponding paper) in using a revised representation of finite state machines and by a focus on executable definitions. 
    
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
