joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Introductie headers weg. Missend haakje. TOC.

Browse source
This commit is contained in:
Joshua Moerman 2018-10-31 11:46:08 +01:00
parent a9bbb8e5d2
commit 024d290b66
6 changed files with 6 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
content/applying-automata-learning.tex
View file

@ -21,9 +21,6 @@ To the best of our knowledge, this is the first paper in which active automata l
\stopabstract \stopabstract
\startsection
[title={Introduction}]
Once they have high-level models of the behaviour of software components, software engineers can construct better software in less time. Once they have high-level models of the behaviour of software components, software engineers can construct better software in less time.
A key problem in practice, however, is the construction of models for existing software components, for which no or only limited documentation is available. A key problem in practice, however, is the construction of models for existing software components, for which no or only limited documentation is available.
@ -88,7 +85,6 @@ All the models for the ESM case study together with the learning and testing sta
\todo{Link naar nieuwe benchmark site} \todo{Link naar nieuwe benchmark site}
\stopsection
\startsection \startsection
[title={Engine Status Manager}, [title={Engine Status Manager},
reference=sec:esm] reference=sec:esm]

4
content/introduction.tex
View file

@ -139,7 +139,7 @@ learning embedded controller software \cite[DBLP:conf/icfem/SmeenkMVJ15], learni
\stopsubsection \stopsubsection
\stopsection \stopsection
\startsection \startsection
[title={Testing Techniques for Automata}] [title={Testing Techniques}]
\todo{Even lang maken als Nominal Techniques.} \todo{Even lang maken als Nominal Techniques.}
@ -164,7 +164,7 @@ More background and other related problems, as well as their complexity results,
\stopsection \stopsection
\startsection \startsection
[title={Nominal Techniques for Automata}] [title={Nominal Techniques}]
In the second part of this thesis, I will present results related to \emph{nominal automata}. In the second part of this thesis, I will present results related to \emph{nominal automata}.
Usually, nominal techniques are introduced in order to solve problems involving name binding in topics like lambda calculus. Usually, nominal techniques are introduced in order to solve problems involving name binding in topics like lambda calculus.

4
content/learning-nominal-automata.tex
View file

@ -15,9 +15,6 @@ An implementation using a recently developed Haskell library for nominal computa
\stopabstract \stopabstract
\startsection
[title={Introduction}]
Automata are a well established computational abstraction with a wide range of applications, including modelling and verification of (security) protocols, hardware, and software systems. Automata are a well established computational abstraction with a wide range of applications, including modelling and verification of (security) protocols, hardware, and software systems.
In an ideal world, a model would be available before a system or protocol is deployed in order to provide ample opportunity for checking important properties that must hold and only then the actual system would be synthesised from the verified model. In an ideal world, a model would be available before a system or protocol is deployed in order to provide ample opportunity for checking important properties that must hold and only then the actual system would be synthesised from the verified model.
Unfortunately, this is not at all the reality: Unfortunately, this is not at all the reality:
@ -65,7 +62,6 @@ In \in{Section}[sec:nondet], we describe an algorithm to learn nominal non-deter
\in{Section}[sec:related] contains a discussion of related work. We conclude the paper with a discussion section where also future directions are presented. \in{Section}[sec:related] contains a discussion of related work. We conclude the paper with a discussion section where also future directions are presented.
\stopsection
\startsection \startsection
[title={Overview of the Approach}, [title={Overview of the Approach},
reference=sec:overview] reference=sec:overview]

6
content/minimal-separating-sequences.tex
View file

@ -18,9 +18,6 @@ algorithm is empirically verified and compared to the traditional algorithm.
\stopabstract \stopabstract
\startsection
[title={Introduction}]
In diverse areas of computer science and engineering, systems can be modelled by \emph{finite state machines} (FSMs). In diverse areas of computer science and engineering, systems can be modelled by \emph{finite state machines} (FSMs).
One of the cornerstones of automata theory is minimisation of such machines (and many variation thereof). One of the cornerstones of automata theory is minimisation of such machines (and many variation thereof).
In this process one obtains an equivalent minimal FSM, where states are different if and only if they have different behaviour. In this process one obtains an equivalent minimal FSM, where states are different if and only if they have different behaviour.
@ -43,7 +40,6 @@ It consists of applying sequences of inputs to the implementation, and comparing
Minimal separating sequences are used in many test generation methods \cite[DBLP:journals/infsof/DorofeevaEMCY10]. Therefore, our algorithm can be used to improve these methods. Minimal separating sequences are used in many test generation methods \cite[DBLP:journals/infsof/DorofeevaEMCY10]. Therefore, our algorithm can be used to improve these methods.
\stopsection
\startsection \startsection
[title={Preliminaries}] [title={Preliminaries}]
@ -536,7 +532,7 @@ A state $s$ is in at most $\log_{2} n$ sets $\delta^{-1}(l(u), a)$, where $u$ is
If we now quantify over all transitions, we immediately get the following result. If we now quantify over all transitions, we immediately get the following result.
We note that the number of blue nodes is at most $n-1$, but since this fact is not used, we leave this to the reader. We note that the number of blue nodes is at most $n-1$, but since this fact is not used, we leave this to the reader.
\startcorollary[reference=cor:count-all \startcorollary[reference=cor:count-all]
Let $\mathcal{B}$ denote the set of blue nodes and define Let $\mathcal{B}$ denote the set of blue nodes and define
\startformula \startformula
\mathcal{X} = \{ (b, a, s) \,|\, b \in \mathcal{B}, a \in I, s \in \delta^{-1}(l(b), a) \}. \mathcal{X} = \{ (b, a, s) \,|\, b \in \mathcal{B}, a \in I, s \in \delta^{-1}(l(b), a) \}.

4
content/ordered-nominal-sets.tex
View file

@ -19,9 +19,6 @@ In both cases, \ONS{} is competitive compared to existing implementations and ou
\stopabstract \stopabstract
\startsection
[title={Introduction}]
Automata over infinite alphabets are natural models for programs with unbounded data domains. Automata over infinite alphabets are natural models for programs with unbounded data domains.
Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[DBLP:journals/corr/BojanczykKL14, DBLP:conf/cav/DAntoniV17, DBLP:journals/corr/GrigoreT16, DBLP:journals/tcs/KaminskiF94, MontanariP97, Segoufin06] and references therein). Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[DBLP:journals/corr/BojanczykKL14, DBLP:conf/cav/DAntoniV17, DBLP:journals/corr/GrigoreT16, DBLP:journals/tcs/KaminskiF94, MontanariP97, Segoufin06] and references therein).
Typical infinite alphabets include sequence numbers, timestamps, and identifiers. Typical infinite alphabets include sequence numbers, timestamps, and identifiers.
@ -76,7 +73,6 @@ The structure of the paper is as follows.
Related work is discussed in \in{Section}[sec:related], and future work in \in{Section}[sec:fw]. Related work is discussed in \in{Section}[sec:related], and future work in \in{Section}[sec:fw].
\stopsection
\startsection \startsection
[title={Nominal sets}, [title={Nominal sets},
reference=sec:nomsets] reference=sec:nomsets]

5
environment/headers.tex
View file

@ -2,12 +2,13 @@
% TOC related % TOC related
\setupcombinedlist[content][list={part,chapter,section}] \setupcombinedlist[content][list={part,chapter,section}]
\setuplist[section][margin=1cm, headnumber=no]
% How numbers are shown % How numbers are shown
\setuphead[part][placehead=yes, align=middle, sectionstarter=Part , sectionstopper=:] \setuphead[part][placehead=yes, align=middle, sectionstarter=Part , sectionstopper=:]
\setuphead[chapter][sectionsegments=chapter, command=\MyChapter] \setuphead[chapter][sectionsegments=chapter, command=\MyChapter]
\setuphead[section][sectionsegments=chapter:section] \setuphead[section][sectionsegments=section]
\setuphead[subsection][sectionsegments=chapter:section:subsection] \setuphead[subsection][sectionsegments=section:subsection]
\define[2]\MyChapter \define[2]\MyChapter
{\framed[frame=off, width=max, align={flushleft,nothyphenated,verytolerant}, offset=0cm, toffset=1cm, boffset=1cm]{#1\\#2}} {\framed[frame=off, width=max, align={flushleft,nothyphenated,verytolerant}, offset=0cm, toffset=1cm, boffset=1cm]{#1\\#2}}