Modely a verifikace chování systémů - NSWX101
Anglický název: System Behaviour Models and Verification
Zajišťuje: Studijní oddělení (32-STUD)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2019
Semestr: zimní
E-Kredity: 6
Rozsah, examinace: zimní s.:2/2, Z+Zk [HT]
Počet míst: neomezen
Minimální obsazenost: neomezen
4EU+: ne
Virtuální mobilita / počet míst pro virtuální mobilitu: ne
Stav předmětu: vyučován
Jazyk výuky: angličtina
Způsob výuky: prezenční
Způsob výuky: prezenční
Je zajišťováno předmětem: NSWI101
Další informace: http://d3s.mff.cuni.cz/teaching/nswi101
Garant: prof. Ing. František Plášil, DrSc.
doc. RNDr. Jan Kofroň, Ph.D.
Třída: Informatika Mgr. - volitelný
Kategorizace předmětu: Informatika > Softwarové inženýrství
Prerekvizity : {NXXX010, NXXX026, NXXX027, NXXX028, NXXX029, NXXX032, NXXX034, NXXX035, NXXX068}
Neslučitelnost : NSWI101
Záměnnost : NSWI101
Výsledky anket   Termíny zkoušek   Rozvrh ZS   Nástěnka   
Anotace -
Základní principy popisu chování paralelních a distribuovaných systémů. Equivalence checking a model checking - postupy a nástroje. Předmět je vyučován v anglickém jazyce.
Poslední úprava: Katedry Tajemník (30.04.2012)
Podmínky zakončení předmětu - angličtina

For successful passing of the course, the students are required to submit their homeworks before the deadline specified at the lectures, labs, and the course web page (all of them).

Poslední úprava: Kofroň Jan, doc. RNDr., Ph.D. (06.10.2017)
Literatura -

P. Regan, S. Hamilton: NASA's Mission Reliable, IEEE Computer, vol. 37, no. 1, Jan 2004

G. J. Holzmann: The Spin Model Checker, Addison Wesley, 2003

E. M. Clarke, Jr., O. Grumberg, D. A. Peled: Model Checking, MIT Press, 2002

J. A. Bergstra, A. Ponse, S. A. Smolka: Handbook of Process Algebra, Elsevier 2001

R. Milner: Communication and Concurrency, Prentice Hall 1989

C. Stirling: Modal and Temporal Properties of Processes, Springer 2001

F. Plasil, S. Visnovsky: Behavior Protocols for Software Components, IEEE Transactions on Software Engineering, vol. 28, no. 11, Nov 2002

J. Adamek, F. Plasil: Component Composition Errors and Update Atomicity: Static Analysis, Journal of Software Maintenance and Evolution: Research and Practice, 2005

D. Engler: Static analysis versus software model checking for bug finding, VMCAI'04

Poslední úprava: Adámek Jiří, RNDr., Ph.D. (28.08.2006)
Požadavky ke zkoušce - angličtina

For getting the credits, it is necessary to submit solutions of the homework assignments and pass the written exam.

Poslední úprava: Kofroň Jan, doc. RNDr., Ph.D. (03.10.2017)
Sylabus -

1. Matematické striktury pro modelování chování system, ling, labeled transition systems, Kripkeho struktury.

2. Equivalence checking.

3. Model checking.

4. Softwarové nástroje pro model checking.

5. Specifikace a verifice real-time systémů.

6. Procesové algebry.

Poslední úprava: Katedry Tajemník (15.05.2013)