Verification of Systems
| Keywords |
| Classification |
Keyword |
| OFICIAL |
Computer Science |
Instance: 2021/2022 - 1S
Cycles of Study/Courses
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
No specific requirements to attend exams.
Calculation formula of final grade
The final grade is classification of the final exam.
Minimum grade: 9.5 over 20
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