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 do 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í
• Další informace: http://d3s.mff.cuni.cz/teaching/nswi101
• Garant: prof. Ing. František Plášil, DrSc.; doc. RNDr. Jan Kofroň, Ph.D.
• Vyučující: doc. RNDr. Jan Kofroň, Ph.D.; prof. Ing. František Plášil, DrSc.
• Třída: Informatika Mgr. - volitelný
• Kategorizace předmětu: Informatika > Softwarové inženýrství
• Je prerekvizitou pro: NSWI136

Anotace

čeština

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)

angličtina

Basic concepts of behavior description of parallel and distributed systems. Equivalence checking and model checking techniques and tools.

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

Literatura

čeština

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)

angličtina

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

Poslední úprava: T_KSI (30.04.2008)

Sylabus

čeština

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)

angličtina

1. Mathematical structures for behavior modeling, labeled transition systems, Kripke structures.

2. Equivalence checking.

3. Model checking.

4. Software tools for model checking.

5. Specification and verification of real time systems.

6. Process algebras.

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