SubjectsSubjects(version: 941)
Course, academic year 2023/2024
   Login via CAS
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
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:
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 -
Last update: Tajemník Katedry (30.04.2012)
Basic concepts of behavior description of parallel and distributed systems. Equivalence checking and model checking techniques and tools.
Course completion requirements
Last update: doc. RNDr. Jan Kofroň, Ph.D. (06.10.2017)

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

Literature -
Last update: T_KSI (30.04.2008)

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

Requirements to the exam
Last update: doc. RNDr. Jan Kofroň, Ph.D. (03.10.2017)

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

Syllabus -
Last update: Tajemník Katedry (15.05.2013)

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.

Charles University | Information system of Charles University |