System Behaviour Models and Verification - NSWX101

• Title: Modely a verifikace chování systémů
• Guaranteed by: Student Affairs Department (32-STUD)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2019
• Semester: winter
• E-Credits: 6
• Hours per week, examination: winter s.:2/2, C+Ex [HT]
• Capacity: unlimited
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: taught
• Language: English
• Teaching methods: full-time
• Teaching methods: full-time
• Is provided by: NSWI101
• Additional information: http://d3s.mff.cuni.cz/teaching/nswi101
• Guarantor: prof. Ing. František Plášil, DrSc.; doc. RNDr. Jan Kofroň, Ph.D.
• Class: Informatika Mgr. - volitelný
• Classification: Informatics > Software Engineering
• Pre-requisite : {NXXX010, NXXX026, NXXX027, NXXX028, NXXX029, NXXX032, NXXX034, NXXX035, NXXX068}
• Incompatibility : NSWI101
• Interchangeability : NSWI101

Annotation

English

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

Last update: Katedry Tajemník (30.04.2012)

Czech

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.

Last update: Katedry Tajemník (30.04.2012)

Course completion requirements

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).

Last update: Kofroň Jan, doc. RNDr., Ph.D. (06.10.2017)

Literature

English

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

Last update: T_KSI (30.04.2008)

Czech

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

Last update: Adámek Jiří, RNDr., Ph.D. (28.08.2006)

Requirements to the exam

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

Last update: Kofroň Jan, doc. RNDr., Ph.D. (03.10.2017)

Syllabus

English

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.

Last update: Katedry Tajemník (15.05.2013)

Czech

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.

Last update: Katedry Tajemník (15.05.2013)