Formální analýza a verifikace

• 26 hod. přednášky
• 26 hod. projekty

Studenti jsou obeznámení s principy a metodami formální analýzy a verifikace a s jejím využitím při návrhu systémů, u nichž je kladen důraz na jejich korektní funkčnost. Studenti znají možnosti a základní způsoby použití počítačových nástrojů, jenž formální analýzu a verifikaci podporují.

Získané povědomí o významu a možnostech uplatnění formálních metod při vývoji různých typů systémů a o jejich rostoucím nasazení v praxi.

Cílem předmětu je představit studentům formální analýzu a verifikaci jako moderní a perspektivní metodu automatizovaného ověřování vlastností různých typů systémů, u nichž je kladen důraz na bezchybnou funkci (např. ovladačů a jiných částí operačních systémů, řídících programů, workflow, komunikačních protokolů, částí hardware apod.). Předmět seznamuje studenty jak s teoretickými základy dané oblasti, s počítačovými nástroji na nich založenými, tak i s úspěšnými aplikacemi formální analýzy a verifikace v praxi (Intel, Nasa, Microsoft, Ericsson, Nokia, ...).

Nejsou žádné prerekvizity.

• Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
• Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
• Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. (Část věnovaná statické analýze.)
• Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
• Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429-528. Springer-Verlag, 1998.
• Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
• Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.
• Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
• Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
• Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008.
• Bertot Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer, 2010.
• Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
• Materiály aktuálně volně dostupné na Internetu, a to zejména články a dokumentace týkající se počítačových nástrojů pro formální analýzu a verifikaci.

• Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
• Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
• Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.

1. Vymezení pojmu "formální analýza a verifikace". Možnosti a přínos formální analýzy a verifikace. Struktura (automatizovaného) procesu formální analýzy a verifikace. Dokazování teorémů, použití stavových prostorů, stavová exploze.
2. Stavový prostor, cesty stavovým prostorem, abstrakce stavů a přechodů. Prokládání a paralelismus. Lineární a větvící se logický čas. Bezpečnost, živost a spravedlivost.
3. Stručný přehled běžně používaných modelovacích jazyků (sítě konečných automatů, Petriho sítě, specialiazované paralelní jazyky, aj.). Specifikační a dotazovací jazyky. Statistiky na úrovni stavových prostorů a modelovacích jazyků. Instrumentace modelů, Büchiho automaty, testery.
4. Temporální logiky. LTL, CTL, CTL*, mí-kalkul. Vztah temporálních logik a automatů. Indexované temporální logiky.
5. Procesní algebry. Zobecněný pohled na procesní algebry, jejich vztah ke stavovým prostorům, operátory paralelní kompozice a ukrývání. Různé typy ekvivalencí a uspořádání procesů, možnosti jejich ověřování.
6. Výpočetní složitost analýzy a verifikace. Složitost ve vztahu k velikosti stavových prostorů a ve vztahu k velikosti modelů. Souvislost paměťových a časových nároků metod formální analýzy a verifikace.
7. Redukce stavových prostorů. Přehled různých přístupů k redukci stavových prostorů, propojení algoritmů redukce a algoritmů generování a využití stavových prostorů. Abstrakce modelů, úpravy modelů. Kompozicionalita.
8. Redukce stavových prostorů. Binární rozhodovací diagramy a symbolické metody. Hashování stavů na jeden bit. Redukce stavových prostorů na základě symetrií v chování modelovaných systémů a na základě částečného uspořádání akcí.
9. Počítačové nástroje podporující formální analýzu a verifikaci založenou na využití stavových prostorů. Spin, Slam, Java PathFinder, Zing, SMV aj. (dle aktuální situace v oboru).
10. Přehled úspěšných aplikací formální analýzy a verifikace v oblasti vestavěných systémů, protokolového inženýrství, řídicích systémů, workflow systémů, apod.
11. Systémy pracující v reálném čase. Logický a fyzický čas. Bezpečnost, živost a realizovatelnost v reálném čase. Modelovací a specifikační jazyky v oblasti reálného času, časované automaty, temporální logiky s reálným časem.
12. Práce se stavovými prostory systémů pracujících v reálném čase, regiony, zóny. Automatizované nástroje pro formální analýzu a verifikaci systémů s reálným časem (Uppaal, Kronos, TReX, ...) a jejich aplikace. Hybridní systémy (HyTech).
13. Dokazování teorémů. Principy, automatizovaná podpora (PVS, aj.), aplikace. Kombinace dokazování teorémů a metod založených na stavových prostorech.

Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.

Získání alespoň 50% možného bodového zisku z domácích úkolů.

• Dva opravované domácí úlohy - každý za 15 bodů.
• Závěrečná písemná zkouška - 70 bodů.
• Podmínka zápočtu: min. 15 bodů získaných v průběhu semestru.
• Hranice pro úspěšnou zkoušku podle pravidel ECTS - 50 bodů.