Formální metody a specifikace

Přednášející:

Stefan Ratschan (gar.)

Cvičící:

Stefan Ratschan (gar.)

Předmět zajišťuje:

katedra softwarového inženýrství

Anotace:

Studenti dokážou formálně popisovat sémantiku software a používat logické uvažování pro konstrukci správně fungujícího software. Naučí se použít některé programové nástroje, které slouží pro dokazování \r

Požadavky:

Znalost základních pojmů matematické logiky a teorie množin, schopnost je používat.

Osnova přednášek:

1. Specifikace programů a základy praktické logiky

2. Logické teorie a modelování datových struktur

3. Operační sémantika programů

4. Omezená správnost programů

5. Ověření neomezené správnosti programů

6. Terminace, totální správnost programů

7. Formální metody pro vestavěné systémy

Osnova cvičení:

Cvičení materiálu z přednášky.

Cíle studia:

Cílem předmětu je poskytnout studentům schopnost používat formální způsoby uvažování při vývoji software. To na jednu stranu zahrnuje schopnost založit své vlastní vývojářské činnosti na logickém úsudku, a to i v prostředí, ve kterém se nepoužívají formální metody. Na druhou stranu to zahrnuje schopnost používání automatizovaných formálních metod a přístrojů, které podporují proces vývoje softwaru.

Studijní materiály:

Aaron R. Bradley and Zohar Manna: ''The Calculus of Computation'', Springer Verlag, 2007

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled: ''Model Checking'', MIT Press, 1999

Zohar Manna and Amir Pnueli: ''Temporal Verification of Reactive Systems'', Springer Verlag, 1995

Glynn Winskel: ''Formal Semantics of Programming Languages'', MIT Press, Cambridge, Massachusetts, 1993

Poznámka:

Rozsah=prednasky+proseminare+cviceni2p+1c, Prednasejici: Dipl.-Ing. Dr. techn. Stefan Ratschan

Rozvrh na zimní semestr 2011/2012:

Rozvrh není připraven

Rozvrh na letní semestr 2011/2012:

	06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Po
Út	místnost T9:346 Ratschan S. 16:15–17:45 LICHÝ TÝDEN (přednášková par. 1 paralelka 101) Dejvice NBFIT učebnamístnost T9:346 Ratschan S. 18:00–19:30 LICHÝ TÝDEN (přednášková par. 1 paralelka 103) Dejvice NBFIT učebna místnost T9:346 Ratschan S. 16:15–17:45 SUDÝ TÝDEN (přednášková par. 1 paralelka 102) Dejvice NBFIT učebna
St	místnost T9:349 Ratschan S. 14:30–16:00 (přednášková par. 1) Dejvice NBFIT místnost
Čt
Pá

Předmět je součástí následujících studijních plánů:

• Zaměření Softwarové inženýrství - verze pro ty, kteří se zapsali v roce 2010 (povinný předmět zaměření)
• Zaměření Softwarové inženýrství - verze pro ty, kteří se zapsali v roce 2011 (povinný předmět zaměření)
• Zaměření Softwarové inženýrství - verze pro ty, kteří se zapsali v roce 2012 (povinný předmět zaměření)