PředmětyPředměty(verze: 790)
Předmět, akademický rok 2016/2017
   Přihlásit přes CAS
Modely a verifikace chování systémů - NSWI101
Anglický název: System Behaviour Models and Verification
Zajišťuje: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2015
Semestr: zimní
E-Kredity: 6
Rozsah, examinace: zimní s.:2/2 Z+Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: vyučován
Jazyk výuky: angličtina
Způsob výuky: prezenční
Další informace: http://d3s.mff.cuni.cz/teaching/nswi101
Garant: prof. Ing. František Plášil, DrSc.
RNDr. Jan Kofroň, Ph.D.
Třída: Informatika Mgr. - volitelný
Kategorizace předmětu: Informatika > Softwarové inženýrství
Anotace -
Poslední úprava: Tajemník Katedry (30.04.2012)

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.
Literatura -
Poslední úprava: RNDr. Jiří Adámek, Ph.D. (28.08.2006)

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

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

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.

 
Univerzita Karlova | Informační systém UK