source: Deliverables/D4.1/ITP-Paper/itp-2011.tex @ 509

Last change on this file since 509 was 509, checked in by sacerdot, 8 years ago

Background.

File size: 24.4 KB
Line 
1\documentclass{llncs}
2
3\usepackage{amsfonts}
4\usepackage{amsmath}
5\usepackage{amssymb} 
6\usepackage[english]{babel}
7\usepackage{color}
8\usepackage{graphicx}
9\usepackage[utf8x]{inputenc}
10\usepackage{listings}
11\usepackage{microtype}
12\usepackage{stmaryrd}
13\usepackage{url}
14
15\lstdefinelanguage{matita-ocaml}
16  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
17   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
18   morekeywords={[3]type,of},
19   mathescape=true,
20  }
21\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
22        keywordstyle=\color{red}\bfseries,
23        keywordstyle=[2]\color{blue},
24        keywordstyle=[3]\color{blue}\bfseries,
25        commentstyle=\color{green},
26        stringstyle=\color{blue},
27        showspaces=false,showstringspaces=false}
28\lstset{extendedchars=false}
29\lstset{inputencoding=utf8x}
30\DeclareUnicodeCharacter{8797}{:=}
31\DeclareUnicodeCharacter{10746}{++}
32\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
33\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
34
35\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
36\authorrunning{C. Sacerdoti Coen and D. P. Mulligan}
37\title{An executable formalisation of the MCS-51 microprocessor in Matita}
38\titlerunning{An executable formalisation of the MCS-51}
39\institute{Dipartimento di Scienze dell'Informazione, University of Bologna}
40
41\begin{document}
42
43\maketitle
44
45\begin{abstract}
46We summarise our formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
47The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
48
49We proceeded in two stages, first implementing in O'Caml a prototype emulator, where bugs could be `ironed out' quickly.
50We then ported our O'Caml emulator to Matita's internal language.
51Though mostly straight-forward, this porting presented multiple problems.
52Of particular interest is how we handle the extreme non-orthoganality of the MSC-51's instruction set.
53In O'Caml, this was handled through heavy use of polymorphic variants.
54In Matita, we achieve the same effect through a non-standard use of dependent types.
55
56Both the O'Caml and Matita emulators are `executable'.
57Assembly programs may be animated within Matita, producing a trace of instructions executed.
58
59Our formalisation is a major component of the ongoing EU-funded CerCo project.
60\end{abstract}
61
62%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
63% SECTION                                                                      %
64%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
65\section{Background}
66\label{sect.introduction}
67
68Formal methods are aimed at increasing our confidence in our software and
69hardware artifacts. Ideally, in the future we would like all artifacts to be
70equipped with a formal specification and a proof of correctness of the
71implementation. Nowadays practically all programs are written in high level
72languages and then compiled into low level ones. Thus the specifications are
73also given at high level and correctness is proved reasoning automatically
74or interactively on the source code. The code that is actually run, however,
75is the object code generated by the compiler.
76
77A few simple questions then arise:
78What properties are preserved during compilation?
79What properties are affected by the compilation strategy?
80To what extent can you trust your compiler in preserving those properties?
81
82Compiler verification, as of late, is a `hot topic' in computer science
83research. So far, it has been focused on the first and last question only.
84In particular, the attention has been put only on extensional properties,
85which are easily preserved during compilation:
86it is sufficient to completely preserve the denotational semantics of the
87input program.
88
89The situation is definitely more complex when we also take in account
90intesional properties of programs, like space, time or energy spent into
91computation and transmission of data. To express this properties and to
92reason on them we are forced to adopt a cost model that assigns a cost to
93single instructions or to blocks of instructions. Morally, we would like to
94have a compositional cost model that assigns the same cost to all occurrences
95of one instruction. However, compiler optimizations are inherently non
96compositional: each occurrence of an high level instruction is usually compiled
97in a different way according to the surrounding instructions. Hence the cost
98model is affected by compilation and thus all intensional specifications are as
99well.
100
101In the EU Project CerCo (Certified Complexity) we will approach the problem
102by developing a compiler that induces the cost model on the source code by
103assigning to each block of high level instructions the cost associated to the
104obtained object code. The cost model will thus be inherently non compositional,
105but it can be extremely \emph{precise}, capturing the realistic cost. In
106particular, we already have a prototype where no approximation of the cost
107is provided at all. The natural applications of our approach are then in the
108domain of hard real time programs, where the user can certify the meeting of
109all dealines while fully exploiting the computational time, that would be
110wasted in case of over-estimation of the costs.
111
112Other applications of our approach are in the domain of compiler verification
113itself. For instance, an extensional specification of an optimization is useless
114since it grants preservation of the semantics without stating that the cost
115(in space or time) of the optimized code should be lower. Another example is
116completeness and correctness of the compilation process in presence of
117space constraints: the compiler could refuse a source
118program for an embedded system when the size of the compiled code exceeds the
119available ROM size. Moreover, preservation of the semantics must be required
120only for those programs that do not exhausts their stack/heap space. Hence the
121statement of completeness of the compiler must take in account the realistic
122cost model.
123
124In the methodology proposed in CerCo we assume to be able to compute on the
125object code exact and realistic costs for sequential blocks of instructions.
126With modern processors, it is possible~\cite{??,??,??}, but difficult,
127to compute exact costs or to reasonably approximate them, since the execution
128of the program itself has an influence on the speed of processing. This is due
129mainly to caching effects and memory effects in the processor, used, for
130instance, to perform branch prediction. For this reason, at the current stage
131of CerCo we decided to focus on 8-bits microprocessors that are still widely
132used in embedded systems and whose cost model is easily predictable.
133
134In particular, we have fully formalized an executable formal semantics of
135the Family of 8 bits Freescale Microprocessors~\cite{oliboni} and a similar
136one for the MCS-51 microprocessors. The latter is the one described in this
137paper. The main focus of the formalization has been on capturing the
138intensional behaviour of the processor. The main problems we have faced,
139however, are mainly due to the extreme unorthogonality of the memory model
140and instruction sets of the MCS-51 microprocessors. To cope with this
141unorthogonality and to have executability, we have exploited the dependent
142type system of the interactive theorem prover Matita.
143
144%Compiler verification, as of late, is a `hot topic' in computer science research.
145%This rapidly growing field is motivated by one simple question: `to what extent can you trust your compiler?'
146%Existing verification efforts have broadly focussed on \emph{semantic correctness}, that is, creating a compiler that is guaranteed to preserve the semantics of a program during the compilation process.
147%However, there is another important facet of correctness that has not garnered much attention, that is, correctness with respect to some intensional properties of the program to be compiled.
148
149\subsection{The 8051/8052}
150\label{subsect.8051-8052}
151
152The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
153Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
154Further, the processor and its immediate successor, the 8052, is still manufactured by a host of semiconductor suppliers---many of them European---including Atmel, Siemens Semiconductor, NXP (formerly Phillips Semiconductor), Texas Instruments, and Maxim (formerly Dallas Semiconductor).
155
156The 8051 is a well documented processor, and has the additional support of numerous open source and commercial tools, such as compilers for high-level languages and emulators.
157For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C, and other compilers targeting the 8051 for BASIC, Forth and Modula-2 are also extant.
158An open source emulator for the processor, MCU8051 IDE, is also available.
159
160\begin{figure}[t]
161\begin{center}
162\includegraphics[scale=0.5]{memorylayout.png}
163\end{center}
164\caption{High level overview of the 8051 memory layout}
165\label{fig.memory.layout}
166\end{figure}
167
168The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
169A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
170
171Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
172Internal memory, commonly provided on the die itself with fast access, is further divided into 128 bytes of internal RAM and numerous Special Function Registers (SFRs) which control the operation of the processor.
173Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
174These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
175Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
176What remains of the IRAM may be treated as general purpose memory.
177A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}.
178
179External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
180XRAM is accessed using a dedicated instruction.
181External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
182However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
183
184Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
185As the latter two addressing modes hint, there are some restrictions enforced by the 8051 and its derivatives on which addressing modes may be used with specific types of memory.
186For instance, the 128 bytes of extra internal RAM that the 8052 features cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used.
187
188The 8051 series possesses an eight bit Arithmetic and Logic Unit (ALU), with a wide variety of instructions for performing arithmetic and logical operations on bits and integers.
189Further, the processor possesses two eight bit general purpose accumulators, A and B.
190
191Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
192Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
193(The 8052 provides an additional sixteen bit timer.)
194As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
195
196The programmer may take advantage of the interrupt mechanism that the processor provides.
197This is especially useful when dealing with input or output involving the serial device, as an interrupt can be set when a whole character is sent or received via the serial port.
198
199Interrupts immediately halt the flow of execution of the processor, and cause the program counter to jump to a fixed address, where the requisite interrupt handler is stored.
200However, interrupts may be set to one of two priorities: low and high.
201The interrupt handler of an interrupt with high priority is executed ahead of the interrupt handler of an interrupt of lower priority, interrupting a currently executing handler of lower priority, if necessary.
202
203The 8051 has interrupts disabled by default.
204The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
205Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
206
207\begin{figure}[t]
208\begin{center}
209\includegraphics[scale=0.5]{iramlayout.png}
210\end{center}
211\caption{Schematic view of 8051 IRAM layout}
212\label{fig.iram.layout}
213\end{figure}
214
215%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
216% SECTION                                                                      %
217%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
218\subsection{The CerCo project}
219\label{subsect.cerco.project}
220
221The CerCo project (`Certified Complexity') is a current European FeT-Open project incorporating three sites---the Universities of Bologna, Edinburgh and Paris Diderot 7---throughout the European Union.
222The ultimate aim of the project is to produce a certified compiler for a large subset of the C programming language targetting a microprocessor used in embedded systems.
223In this respect, the CerCo project bears a deal of similarity with CompCert, another European funded project.
224However, we see a number of important differences between the aims of the two projects.
225\begin{enumerate}
226\item
227The CerCo project aims to allow reasoning on aspects of the intensional properties of C programs.
228That is,
229\item
230The CompCert project compiled a subset of C down to the assembly level.
231A semantics for assembly language was provided.
232\end{enumerate}
233
234%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
235% SECTION                                                                      %
236%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
237\subsection{Overview of paper}
238\label{subsect.overview.paper}
239
240In Section~\ref{sect.development.strategy} we provide a brief overview of how we designed and implemented the formalised microprocessor emulator.
241In Section~\ref{sect.design.issues.formalisation} we describe how we made use of dependent types to handle some of the idiosyncracies of the microprocessor.
242In Section~\ref{sect.related.work} we describe the relation our work has to
243
244%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
245% SECTION                                                                      %
246%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
247\section{From O'Caml prototype to Matita formalisation}
248\label{sect.from.o'caml.prototype.matita.formalisation}
249
250Our implementation progressed in two stages:
251
252\paragraph{O'Caml prototype}
253We began with an emulator written in O'Caml.
254We used this to `iron out' any bugs in our design and implementation within O'Caml's more permissive type system.
255O'Caml's ability to perform file input-output also eased debugging and validation.
256Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
257
258\paragraph{Matita formalisation}
259Matita's syntax is lexically similar to O'Caml's.
260This eased the translation, as large swathes of code were merely copy-pasted with minor modifications.
261However, several major issues had to be addresses when moving from O'Caml to Matita.
262These are now discussed.
263
264%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
265% SECTION                                                                      %
266%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
267\section{Design issues in the formalisation}
268\label{sect.design.issues.formalisation} 
269
270%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
271% SECTION                                                                      %
272%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
273\subsection{Labels and pseudoinstructions}
274\label{subsect.labels.pseudoinstructions}
275
276As part of the CerCo project, a prototype compiler was being developed in parallel with the emulator.
277Easing the design of the compiler was a key objective in implementing the emulator.
278For this reason, we introduced notion of \emph{pseudoinstruction} and \emph{label}.
279
280The MCS-51's instruction set has numerous instructions for unconditional and conditional jumps to memory locations, calling procedures and moving data between memory spaces.
281For instance, the instructions \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP} all perform unconditional jumps.
282However, these instructions differ in how large the maximum size of the offset of the jump to be performed can be.
283Further, all jump instructions require a concrete memory address, to jump to, to be specified.
284Requiring the compiler to compute these offsets, and select appropriate jump instructions, was seen as needleslly burdensome.
285
286Instead, we introduced generic \texttt{Jump}, \texttt{Call} and \texttt{Move} instructions.
287These are expanded into MCS-51 assembly instructions with an assembly phase, prior to program execution.
288Further, we introduced a notion of label (represented by strings), and introduced pseudoinstructions that allow conditional jumps to jump to labels.
289These are also removed during the assembly phase, and replaced by concrete memory addresses and offsets.
290
291%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
292% SECTION                                                                      %
293%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
294\subsection{Putting dependent types to work}
295\label{subsect.putting.dependent.types.to.work}
296
297A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
298For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes.
299
300Such non-orthogonality in the instruction set was handled with the use of polymorphic variants in the O'Caml emulator.
301For instance, we introduced types corresponding to each addressing mode:
302\begin{quote}
303\begin{lstlisting}
304type direct = [ `DIRECT of byte ]
305type indirect = [ `INDIRECT of bit ]
306...
307\end{lstlisting}
308\end{quote}
309Which were then used in our inductive datatype for assembly instructions, as follows:
310\begin{quote}
311\begin{lstlisting}
312type 'addr preinstruction =
313 [ `ADD of acc * [ reg | direct | indirect | data ]
314...
315 | `MOV of
316    (acc * [ reg | direct | indirect | data ],
317     [ reg | indirect ] * [ acc | direct | data ],
318     direct * [ acc | reg | direct | indirect | data ],
319     dptr * data16,
320     carry * bit,
321     bit * carry
322     ) union6
323...
324\end{lstlisting}
325\end{quote}
326Here, \texttt{union6} is a disjoint union type, defined as follows:
327\begin{quote}
328\begin{lstlisting}
329type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
330\end{lstlisting}
331\end{quote}
332For our purposes, the types \texttt{union2} and \texttt{union3} were also necessary.
333
334This polymorphic variant machinery worked well: it allowed us to pattern match
335
336We provide an inductive data type representing all possible addressing modes of 8051 assembly.
337This is the type that functions will pattern match against.
338
339\begin{quote}
340\begin{lstlisting}
341ninductive addressing_mode: Type[0] ≝
342  DIRECT: Byte $\rightarrow$ addressing_mode
343| INDIRECT: Bit $\rightarrow$ addressing_mode
344...
345\end{lstlisting}
346\end{quote}
347However, we also wish to express in the type of our functions the \emph{impossibility} of pattern matching against certain constructors.
348In order to do this, we introduce an inductive type of addressing mode `tags'.
349The constructors of \texttt{addressing\_mode\_tag} are in one-one correspondence with the constructors of \texttt{addressing\_mode}:
350\begin{quote}
351\begin{lstlisting}
352ninductive addressing_mode_tag : Type[0] ≝
353  direct: addressing_mode_tag
354| indirect: addressing_mode_tag
355...
356\end{lstlisting}
357\end{quote}
358We then provide a function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag}, as follows:
359\begin{quote}
360\begin{lstlisting}
361nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
362  match d with
363   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
364   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
365...
366\end{lstlisting}
367\end{quote}
368We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
369\begin{quote}
370\begin{lstlisting}
371nlet rec is_in (n: Nat) (l: Vector addressing_mode_tag n) (A:addressing_mode) on l ≝
372 match l return $\lambda$m.$\lambda$_ :Vector addressing_mode_tag m.Bool with
373  [ VEmpty $\Rightarrow$ false
374  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
375     is_a he A $\vee$ is_in ? tl A ].
376\end{lstlisting}
377\end{quote}
378Here \texttt{VEmpty} and \texttt{VCons} are the two constructors of the \texttt{Vector} data type, and $\mathtt{\vee}$ is inclusive disjunction on Booleans.
379\begin{quote}
380\begin{lstlisting}
381nrecord subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
382{
383  subaddressing_modeel :> addressing_mode;
384  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
385}.
386\end{lstlisting}
387\end{quote}
388We can now provide an inductive type of preinstructions with precise typings:
389\begin{quote}
390\begin{lstlisting}
391ninductive preinstruction (A: Type[0]): Type[0] ≝
392   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
393 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
394...
395\end{lstlisting}
396\end{quote}
397Here $\llbracket - \rrbracket$ is syntax denoting a vector.
398We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
399
400The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
401The previous machinery allows us to state in the type of a function what addressing modes that function expects.
402For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
403\begin{quote}
404\begin{lstlisting}
405ndefinition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
406  $\lambda$s, v, a.
407   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
408     [ DPTR $\Rightarrow$ $\lambda$_: True.
409       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
410       let status := set_8051_sfr s SFR_DPH bu in
411       let status := set_8051_sfr status SFR_DPL bl in
412         status
413     | _ $\Rightarrow$ $\lambda$_: False.
414       match K in False with
415       [
416       ]
417     ] (subaddressing_modein $\ldots$ a).
418\end{lstlisting}
419\end{quote}
420All other cases are discharged by the catch-all at the bottom of the match expression.
421Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
422
423%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
424% SECTION                                                                      %
425%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
426\section{Validation}
427\label{sect.validation}
428
429%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
430% SECTION                                                                      %
431%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
432\section{Related work}
433\label{sect.related.work}
434
435%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
436% SECTION                                                                      %
437%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
438\section{Conclusions}
439\label{sect.conclusions}
440
441\end{document}
Note: See TracBrowser for help on using the repository browser.