1 |
|
2 \documentclass{beamer} |
|
3 |
|
4 |
|
5 \mode<presentation> |
|
6 { |
|
7 \usetheme{Hannover} |
|
8 \setbeamercovered{transparent} |
|
9 } |
|
10 |
|
11 \usepackage[english]{babel} |
|
12 \usepackage[utf8]{inputenc} |
|
13 \usepackage{times} |
|
14 \usepackage[T1]{fontenc} |
|
15 |
|
16 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
17 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
|
18 |
|
19 \title[SPSC in \isac] % (optional, use only with long paper titles) |
|
20 {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac} |
|
21 |
|
22 \subtitle{Baccalaureate Thesis} |
|
23 |
|
24 \author[Ro\v{c}nik] |
|
25 {Jan Rocnik} |
|
26 |
|
27 \institute % (optional, but mostly needed) |
|
28 { |
|
29 Technische Universit\"at Graz\\ |
|
30 Institut f\"ur TODO |
|
31 } |
|
32 |
|
33 % If you have a file called "university-logo-filename.xxx", where xxx |
|
34 % is a graphic format that can be processed by latex or pdflatex, |
|
35 % resp., then you can add a logo as follows: |
|
36 |
|
37 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename} |
|
38 % \logo{\pgfuseimage{university-logo}} |
|
39 |
|
40 |
|
41 |
|
42 % Delete this, if you do not want the table of contents to pop up at |
|
43 % the beginning of each subsection: |
|
44 \AtBeginSubsection[] |
|
45 { |
|
46 \begin{frame}<beamer>{Outline} |
|
47 \tableofcontents[currentsection,currentsubsection] |
|
48 \end{frame} |
|
49 } |
|
50 |
|
51 \begin{document} |
|
52 |
|
53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
54 %% Title Page %% |
|
55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
56 |
|
57 \begin{frame} |
|
58 \titlepage |
|
59 \end{frame} |
|
60 |
|
61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
62 %% Table of Contents %% |
|
63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
64 |
|
65 \begin{frame}{Outline} |
|
66 \tableofcontents |
|
67 % You might wish to add the option [pausesections] |
|
68 \end{frame} |
|
69 |
|
70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
71 %%---------------------------------------------------------------%% |
|
72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
73 |
|
74 \section[Intro]{Introduction} |
|
75 |
|
76 \begin{frame}{Issues to be Accomplished} |
|
77 |
|
78 \begin{itemize} |
|
79 |
|
80 \item What knowledge is already mechanised in \emph{Isabelle}? |
|
81 \item How can missing theorems and definitions be mechanised? |
|
82 \item What is the effort for such mechanisation? |
|
83 \item How do calculations look like, by using mechanised knowledge? |
|
84 \item What problems and subproblems have to be solved? |
|
85 \item Which problems are already implemented in \sisac? |
|
86 \item How are the new problems specified (\sisac)? |
|
87 \item Which variantes of programms in \sisac\ solve the problems? |
|
88 \item What is the contents of the interactiv course material (Figures, etc.)? |
|
89 |
|
90 \end{itemize} |
|
91 \end{frame} |
|
92 |
|
93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
94 %%---------------------------------------------------------------%% |
|
95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
96 |
|
97 \section[Fourier]{Fourier transformation} |
|
98 \subsection[Fourier]{Fourier transform} |
|
99 |
|
100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
101 %% Fourier INTRO %% |
|
102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
103 |
|
104 \begin{frame}\frametitle{Fourier Transformation: Introduction} |
|
105 Possibilities: |
|
106 \begin{itemize} |
|
107 \item Transform operation by using property-tables |
|
108 \item Transform operation by using integral |
|
109 \end{itemize} |
|
110 Also Important: |
|
111 \begin{itemize} |
|
112 \item Visualisation?! |
|
113 \end{itemize} |
|
114 \end{frame} |
|
115 |
|
116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
117 %% Transform expl SPEC %% |
|
118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
119 |
|
120 \begin{frame}\frametitle{Fourier Transformation: Specification} |
|
121 {\footnotesize |
|
122 |
|
123 Determine the fourier transform for the given rectangular impulse: |
|
124 |
|
125 \begin{center} |
|
126 $x(t)= \left\{ |
|
127 \begin{array}{lr} |
|
128 1 & -1\leq t\leq1\\ |
|
129 0 & else |
|
130 \end{array} |
|
131 \right.$ |
|
132 \end{center} |
|
133 |
|
134 \hrulefill |
|
135 |
|
136 \begin{tabbing} |
|
137 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
|
138 \>given \>:\> piecewise\_function \\ |
|
139 \> \> \> \>$fun (x (t::real),\ x=1\ ((t>=-1)\ \&\ (t<=1)),\ x=0)$\\ |
|
140 \>precond \>:\> TODO\\ |
|
141 \>find \>:\> $X(j\cdot\omega)$\\ |
|
142 \>postcond \>:\> TODO\\ |
|
143 \end{tabbing} |
|
144 |
|
145 } |
|
146 \end{frame} |
|
147 |
|
148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
149 %% Transform expl REQ %% |
|
150 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
151 |
|
152 \begin{frame}\frametitle{Fourier Transform: Development effort} |
|
153 {\small |
|
154 \begin{center} |
|
155 \begin{tabular}{l|l|r} |
|
156 requirements & comments &effort\\ \hline\hline |
|
157 solving Intrgrals & simple via propertie table & 20\\ |
|
158 & \emph{real} & MT\\ \hline |
|
159 transformation table & simple transform & 20\\ \hline |
|
160 visualisation & backend & 10\\ \hline |
|
161 example collection & with explanations & 20\\ \hline\hline |
|
162 & & 70-80\\ |
|
163 \end{tabular} |
|
164 \end{center} |
|
165 effort --- in 45min units\\ |
|
166 MT --- thesis ``Integrals'' (mathematics) |
|
167 } |
|
168 \end{frame} |
|
169 |
|
170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
171 %%--------------------FOURIER---Conclusion-----------------------%% |
|
172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
173 |
|
174 \begin{frame}{Fourier Transformation: Summary} |
|
175 \begin{itemize} |
|
176 |
|
177 \item Standard integrals can be solved with tables |
|
178 \item No real integration (yet avaible) |
|
179 \item Math \emph{tricks} difficult to implement |
|
180 |
|
181 |
|
182 \end{itemize} |
|
183 \end{frame} |
|
184 |
|
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
186 %-----------------------------------------------------------------% |
|
187 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
188 |
|
189 \section[LTI Systems]{LTI systems} |
|
190 \subsection[Convolution]{Convolution (Faltung)} |
|
191 |
|
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
193 %% LTI INTRO %% |
|
194 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
195 |
|
196 \begin{frame}\frametitle{Convolution: Introduction} |
|
197 \begin{itemize} |
|
198 \item Calculation include sums |
|
199 \item Demonstrative examples |
|
200 \item Visualisation is important |
|
201 \end{itemize} |
|
202 \end{frame} |
|
203 |
|
204 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
205 %% LTI SPEC %% |
|
206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
207 |
|
208 \begin{frame}\frametitle{Convolution: Specification} |
|
209 {\footnotesize |
|
210 |
|
211 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response: |
|
212 |
|
213 \begin{center} |
|
214 $h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\ |
|
215 $h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$ |
|
216 \end{center} |
|
217 |
|
218 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$. |
|
219 |
|
220 \hrulefill |
|
221 |
|
222 \begin{tabbing} |
|
223 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
|
224 \>given \>:\> Signals h1[n], h2[n] \\ |
|
225 \> \> \> \>((h1[n]=(3/5)\textasciicircum{}n*u[n]),\,h2[n]=(-2/3)\textasciicircum{}n*u[n]))\\ |
|
226 |
|
227 \>precond \>:\> TODO\\ |
|
228 \>find \>:\> $h1[n]\,*\,h2[n]$\\ |
|
229 \>postcond \>:\> TODO\\ |
|
230 \end{tabbing} |
|
231 |
|
232 } |
|
233 \end{frame} |
|
234 |
|
235 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
236 %% LTI REQ %% |
|
237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
238 |
|
239 \begin{frame}\frametitle{Convolution: Development effort} |
|
240 {\small |
|
241 \begin{center} |
|
242 \begin{tabular}{l|l|r} |
|
243 requirements & comments &effort\\ \hline\hline |
|
244 simplify rationals & \sisac & 0\\ \hline |
|
245 define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline |
|
246 simplify sum & termorder & 10\\ |
|
247 & simplify rules & 20\\ |
|
248 & use simplify rationals& 0\\ \hline |
|
249 index adjustments & with unit step & 10\\ \hline |
|
250 example collection & with explanations & 20\\ \hline\hline |
|
251 & & 70-90\\ |
|
252 \end{tabular} |
|
253 \end{center} |
|
254 effort --- in 45min units\\ |
|
255 } |
|
256 \end{frame} |
|
257 |
|
258 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
259 %%--------------------LTI-------Conclusion-----------------------%% |
|
260 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
261 |
|
262 \begin{frame}{Convolution: Summary} |
|
263 \begin{itemize} |
|
264 |
|
265 \item Standard example |
|
266 \item Straight forward |
|
267 \item Challenge are sum limits |
|
268 |
|
269 \end{itemize} |
|
270 \end{frame} |
|
271 |
|
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
273 %-----------------------------------------------------------------% |
|
274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
275 |
|
276 \section[Z-transform]{Z-Transform} |
|
277 \subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform} |
|
278 |
|
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
280 %% Z-Transform INTRO %% |
|
281 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
282 |
|
283 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction} |
|
284 \begin{itemize} |
|
285 \item Pure Transformation is simple to realise with Z-Transform Properties (Table) |
|
286 \item Partial Fraction are just math simplifications |
|
287 \end{itemize} |
|
288 \end{frame} |
|
289 |
|
290 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
291 %% Z-Transform SPEC %% |
|
292 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
293 |
|
294 \begin{frame}\frametitle{(Inverse) Z-Transformation: Specification} |
|
295 {\footnotesize |
|
296 |
|
297 Determine the inverse z transform of the following expression. Hint: applay the partial fraction expansion. |
|
298 |
|
299 \begin{center} |
|
300 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable |
|
301 \end{center} |
|
302 |
|
303 |
|
304 \hrulefill |
|
305 |
|
306 \begin{tabbing} |
|
307 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
|
308 \>given \>:\> Expression of z \\ |
|
309 \> \> \> \>(X (z::complex),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\ |
|
310 \>precond \>:\> TODO\\ |
|
311 \>find \>:\> Expression of n\\ |
|
312 \> \> \> \>$h[n]$\\ |
|
313 \>postcond \>:\> TODO\\ |
|
314 \end{tabbing} |
|
315 |
|
316 } |
|
317 \end{frame} |
|
318 |
|
319 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
320 %% Z expl REQ %% |
|
321 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
322 |
|
323 |
|
324 \begin{frame}\frametitle{(Inverse) Z-Transformation: Development effort} |
|
325 {\small |
|
326 \begin{center} |
|
327 \begin{tabular}{l|l|r} |
|
328 requirements & comments &effort\\ \hline\hline |
|
329 solve for part.fract. & \sisac: degree 2 & 0\\ |
|
330 & complex nomminators & 30\\ |
|
331 & degree > 2 & MT\\ \hline |
|
332 simplify polynomial & \sisac & 0\\ |
|
333 simplify rational & \sisac & 0\\ \hline |
|
334 part.fract.decomposition& degree 2 & \\ |
|
335 & specification, method& 30\\ \hline |
|
336 ${\cal Z}^{-1}$ table & & 20\\ |
|
337 & explanations, figures& 20\\ \hline |
|
338 example collection & with explanations & 20\\ \hline\hline |
|
339 & & 90-120\\ |
|
340 % & & 1 MT |
|
341 \end{tabular} |
|
342 \end{center} |
|
343 effort --- in 45min units\\ |
|
344 MT --- thesis ``factorization'' (mathematics) |
|
345 } |
|
346 \end{frame} |
|
347 |
|
348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
349 %%--------------------Z-TRANS---Conclusion-----------------------%% |
|
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
351 |
|
352 \begin{frame}{(Inverse) Z-Transformation: Summary} |
|
353 \begin{itemize} |
|
354 |
|
355 \item No \emph{higher} math operations |
|
356 \item Different subproblems of math (equation systems, etc.) |
|
357 \item Both directions have the same effort |
|
358 |
|
359 \end{itemize} |
|
360 \end{frame} |
|
361 |
|
362 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
363 %-----------------------------------------------------------------% |
|
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
365 |
|
366 \section[Conclusions]{Conclusions} |
|
367 |
|
368 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
369 %--------------------------DEMONSTRATION--------------------------% |
|
370 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
371 |
|
372 \begin{frame}{Demonstration} |
|
373 |
|
374 \centering{Demonstration} |
|
375 |
|
376 \end{frame} |
|
377 |
|
378 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
379 %--------------------------CONCLUSION-----------------------------% |
|
380 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
381 |
|
382 \begin{frame}{Conclusions} |
|
383 |
|
384 Design Challanges: |
|
385 |
|
386 {\small |
|
387 \begin{itemize} |
|
388 |
|
389 \item Pre and Post conditions |
|
390 \item Exact mathematic behind functions |
|
391 \item Accurate mathematic notation |
|
392 |
|
393 \end{itemize} |
|
394 } |
|
395 |
|
396 Goals: |
|
397 {\small |
|
398 \begin{itemize} |
|
399 |
|
400 \item Spot the power of \sisac |
|
401 \item Implementation of generell but simple math problems |
|
402 \item Setting up a good first guideline (documentation) for furher problem implemenations |
|
403 |
|
404 \end{itemize} |
|
405 |
|
406 \centering{Efforts are only approximations, due we have no \emph{real} experience data!} |
|
407 } |
|
408 |
|
409 \end{frame} |
|
410 |
|
411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
412 %--------------------------TIME LINE------------------------------% |
|
413 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
414 |
|
415 \begin{frame}{Comming up} |
|
416 |
|
417 {\small |
|
418 \begin{tabular}{l r} |
|
419 |
|
420 Juli 2011 & project startup\\ |
|
421 Juli 2011 & information collection, 1st presentation\\ |
|
422 August 2011 & extern traineeship\\ |
|
423 September 2011 & main work\\ |
|
424 after Oktober & finishing, documentation\\ |
|
425 |
|
426 \end{tabular} |
|
427 } |
|
428 |
|
429 \end{frame} |
|
430 |
|
431 |
|
432 \end{document} |
|
433 |
|
434 |
|