Verification of Systems

Code:

CC4084

Acronym:

CC4084

Level:

400

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2022/2023 - 1S

Active?	Yes
Responsible unit:	Department of Computer Science
Course/CS Responsible:	Master in Computer Science

Cycles of Study/Courses

Acronym	No. of Students	Study Plan	Curricular Years	Credits UCN	Credits ECTS	Contact hours	Total Time
M:CC	7	Study plan since 2014/2015	1	-	6	42	162

Teaching language

Suitable for English-speaking students

Objectives

Introduction to formal techniques of verification of computer systems based on models (model checking). 

Learning outcomes and competences

Students should:
- understand the importance of using logic and formal methods in the development of complex computer systems;
- be able to model simple systems and specify properties using temporal logics.

Working method

Presencial

Program

Introduction to model checking.

Modeling of parallel systems: transition systems

Parallelism and communication.

Linear temporal properties: safety, liveliness and fairness.

Introduction to regular properties.

Time logics: linear (LTL) and branched (CTL and CTL *).

Modeling and specification using a model checker

Model checking algorithms for LTL and CTL.

Problem of state explosion. Equivalence of models.

Symbolic model checking: BDDs and OBDDs.

Implementation techniques for model checking.

Decision algorithms based on automata.

Introduction to the verification of timed and probabilistic models.

Mandatory literature

Baier Christel; Principles of model checking. ISBN: 978-0-262-02649-9

Complementary Bibliography

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X

Teaching methods and learning activities

Lectures and case studies.

Evaluation Type

Distributed evaluation with final exam

Assessment Components

designation	Weight (%)
Exame	100,00
Total:	100,00

Amount of time allocated to each course unit

designation	Time (hours)
Estudo autónomo	110,00
Frequência das aulas	52,00
Total:	162,00

Eligibility for exams

- In the middle of the semester there is a non-mandatory test, quoted with 20 points.
- The regular exam consists of two parts. 
-Students must obtain a minimum of 6 values (out of 20) in each of the parts.
- Students with a score of six or more values in the test may choose not to take the first part of the exam and take
the grade obtained in the test for the calculation of the final grade (arithmetic mean).



All the studens can take the resit exam.

Calculation formula of final grade

The final grade F is given by the formula
F = FP*(0.5) + SP*(0.5)

(FP - first part, SP - second part)
FP,SP >= 6 e F >= 9.5

Special assessment (TE, DA, ...)

All students are rated in the same way.

Classification improvement

Students can take the resit exam to raise their grade.

Observations

Notions of propositional and first-order Logic