Okruh Formální metody pro analýzu a verifikaci

Podokruhy:

Formální verifikace a analýza sekvenčních programů

Anotace:
Nejběžnější technikou pro odhalování chyb v programech je stále testování, které umožňuje snadno nalézt mnoho chyb, ale neumožňuje dokázat bezchybnost programu. K tomu slouží metody formální verifikace. Metody analýzy pak mohou být použity k získání informací, které umožní např. optimalizaci během kompilace nebo efektivnější vyhledávání chyb v programech. Otázka pokrývá základní techniky analýzy a verifikace programů.

Osnova:
Formální aspekty testování, míry pokrytí kódu testy, deduktivní a axiomatická programová verifikace, statická analýza a abstraktní interpretace, symbolická exekuce.

Základní studijní materiál:
Doron A. Peled: Software Reliability Methods (kapitoly 7 a 9)
Flemming Nielson, Hanne R. Nielson, and Chris Hankin: Principles of Program Analysis (kapitoly 2 a 4)
James C. King, Symbolic execution and program testing, Communications of the ACM, volume 19, number 7, 1976, 385--394.

Zkoušející: prof. RNDr. Jan Strejček, Ph.D., prof. RNDr. Jiří Barnat, Ph.D.

Verifikace a analýza paralelních programů a reaktivních systémů

Anotace:
Vývoj reaktivních, paralelních, či jinak distribuovaných, systémů je řádově obtížnější a nákladnější, než je tomu u sekvenčních programů. Primárním důvodem pro toto tvrzení je fakt, že chyby návrhu či implementace těchto systémů se projevují náhodně. V rámci této otázky se student seznámí s kompletní technologí analýzy a verifikace uvedených systémů metodou ověřování modelu (angl. model checking).

Osnova:
Modelování a souběžných a reaktivních systémů, formální specifikace požadavků logikami LTL a CTL, využití teorie automatů pro realizaci metody, převod formální specifikace na omega-regulární automaty, enumerativní a symbolické přístupy k metodě ověřování modelu, problém generování stavového prostoru, metody redukce stavového prostoru, reprezentace stavového prostoru, nástroje pro realizaci verifikační metody a jejich implementace.

Základní studijní materiál:
Doron A. Peled: Software Reliability Methods (kapitoly 4-6)
Clarke, Grumberg, Peled: Model checking (kapitoly 2-6,8-10)

Zkoušející: prof. RNDr. Ivana Černá, CSc., prof. RNDr. Jiří Barnat, Ph.D., prof. RNDr. Jan Strejček, Ph.D.

Další doporučená literatura:
C. Baier, J.P. Katoen: Principles of Model Checking
Gerard J. Holzmann: The Spin model checker, primer and reference manual

Specifikace a verifikace nekonečně-stavových systémů

Anotace:
Některé reálné SW systémy je nutné modelovat jako nekonečně stavové. Uchazeč se seznámí s problematikou jaké jsou možnosti a základní metody (konečné) specifikace systémů s nekonečně mnoha stavy a jaké jsou (algoritmické) meze automatické verifikace vlastností těchto systémů.

Osnova:
Způsoby specifikace procesů, Ekvivalence procesů, Rozhodnutelnost problémů ekvivalence, Ověřování modelu nekonečně stavových systémů.

Základní studijní materiál:
Javier Esparza: Grammars as Processes. Formal and Natural Computing 2002, s. 277-297
Wan Fokkink: Introduction to Process Algebra, Springer, 2000, 163 s.
O. Burkart, D. Caucal, F. Moller, B. Steffen: Verification on infinite structures. In J.A. Bergstra et al.: Handbook of Process Algebra, Elsevier, 2001, s. 545-626.

Zkoušející: prof. RNDr. Mojmír Křetínský, CSc., prof. RNDr. Jan Strejček, Ph.D.

Další doporučená literatura:
J.Srba: Roadmap of Infinite Results
Doron A. Peled: Software Reliability Methods (kapitola 8)
R.J.van Glabbeck: The linear time - branching time spectrum I. In J.A.Bergstra et al.: Handbook of Process Algebra, Elsevier, 2001, s.3-100

Modelování a verifikace hybridních systémů a systémů s reálným časem

Anotace:
Interakce softwarových systémů s reálným fyzickým světem, často vynucuje požadavky jež jsou nad rámec logické správnosti vyvíjených systémů. Typickým příkladem jsou požadavky týkající se například tvrdých časových omezení. V rámci této otázky se studenti seznámí s modelovacími formalismy pro popis takovýchto systémů a metodami jejich analýzy.

Osnova:
Hybridní automaty, rozhodnutelnost problému dosažitelnosti, časové automaty, regionová a zónová abstrakce, verifikace temporálních vlastností časových automatů.

Základní studijní materiál:
T. Henzinger: The Theory of Hybrid Automata
C. Baier, J.P. Katoen: Principles of Model Checking (kapitola 9)

Zkoušející: prof. RNDr. Jiří Barnat, Ph.D., doc. RNDr. David Šafránek, Ph.D.

Další doporučená literatura:
John Lygeros: Lecture Notes on Hybrid Systems
Waez, Dingel, Rudie: Timed Automata for the Development of Real-Time Systems


Anotace:
Student se seznámí se základními metodami a technikami z oblasti využití modálních a temporálních logik formální vallidaci a verifikaci počítačových systémů.

Osnova:
Výroková modální logika, dynamická logika, Logiky lineárního času - varianty logik, axiomatizace, rozhodnutelnost a složitost, příklady použití, Logiky větvícího se času  - axiomatizace, rozhodnutelnost a složitost, příklady použití, Modální mu-kalkul - syntaxe a sémantika, alternace pevných bodů, vyjádřování vlastností.

Základní studijní materiál:
C. Stirling, Modal and temporal properties of processes. Springer, 2001.

Zkoušející: prof. RNDr. Luboš Brim, CSc., prof. RNDr. Jan Strejček, Ph.D., prof. RNDr. Jiří Barnat, Ph.D.

Další doporučená literatura:
C. Baier, J.-P. Katoen. Principles of model checking. MIT Press, 2008.
O. Grumberg, D. Peled, E. Clarke. Model checking. Cambridge: MIT Press, 1999.