Formální metody a specifikace

Garant předmětu:

Přednášející:

Cvičící:

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í vlastností softwaru.

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. Symbolické provádění programů

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

Poznámka:

Informace o předmětu a výukové materiály naleznete na https://moodle-vyuka.cvut.cz/course/view.php?id=2728

Další informace:

https://moodle-vyuka.cvut.cz/course/view.php?id=2728

Pro tento předmět se rozvrh nepřipravuje

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

• Mgr. obor Znalostní inženýrství, 2016-2017 (volitelný předmět)
• Mgr. obor Počítačová bezpečnost, 2016-2019 (volitelný předmět)
• Mgr. obor Počítačové systémy a sítě, 2016-2019 (volitelný předmět)
• Mgr. obor Návrh a programování vestavných systémů, 2016-2019 (volitelný předmět)
• Mgr. obor Webové a softwarové inženýrství, zaměření Informační systémy a management, 2016-2019 (volitelný předmět)
• Mgr. obor Webové a softwarové inženýrství, zaměření Softwarové inženýrství, 2016-2019 (povinný předmět zaměření)
• Mgr. obor Webové a softwarové inženýrství, zaměření Webové inženýrství, 2016-2019 (volitelný předmět)
• Mgr. program Informatika, pro fázi studia bez oboru, 2016-2019 (VO)
• Mgr. obor Systémové programování, zaměření Systémové programování, 2016-2019 (volitelný předmět)
• Mgr. obor Systémové programování, zaměření Teoretická informatika, 2016-2017 (volitelný předmět)
• Mgr. specializace Teoretická informatika, 2018-2019 (volitelný předmět)
• Mgr. obor Znalostní inženýrství, 2018-2019 (volitelný předmět)