Formal Methods in System Design

Course Description

Mathematically based specification, development and verification procedures of hardware and software systems, aspiring to enhance the quality of final product and at the same time cut down time-to-market period. Mathematical logic as a foundation for specification languages. Deductive systems. Varieties of formal specification languages. Models of hardware and software system implementations. Specification and verification of computational and reactive systems. Theorem proving and model checking verification procedures. Tools for automated formal system verification. Formal conceptual modeling. Application of formal methods in diverse domains of computer hardware and software engineering.

General Competencies

Students will gain knowledge and skills on real benefits and constrains of using formal methods in systems design. In particular, students will obtain knowledge of target system modeling, specifying desired structural and behavioral properties and applying procedures that check whether these properties were satisfied.

Learning Outcomes

  1. define and state the notion of correct system execution.
  2. distinguish between correct and incorretc system bahavior.
  3. apply formal logic in expressing (desired) system behavior.
  4. analyze and classify the output of tool for formal system verification..
  5. modify the system structure in order to satisfy the desired behavior.
  6. design and integrate or modify tools for formal system verification.
  7. construct formal models of real systems suitable for verification.

Forms of Teaching

Lectures

The course is organized in two cycles. The first cycle consists of 7 weeks of lectures and midterm exam. The second cycle consists of 6 weeks of lectures and final exam.

Exams

Short quizzes (3), homeworks (3), midterm exam, final exam

Grading Method

Continuous Assessment Exam
Type Threshold Percent of Grade Threshold Percent of Grade
Homeworks 0 % 30 % 0 % 30 %
Quizzes 0 % 9 % 0 % 9 %
Mid Term Exam: Written 0 % 25 % 0 %
Final Exam: Written 0 % 36 %
Exam: Written 0 % 61 %

Week by Week Schedule

  1. Course administration, examples pf typical errors in system design. Motivation for acquiring knowledge in applying formal methods throughout the design process. Classification of formal methods.
  2. The role of mathematical logic in specifying and verifying structural and behavioral system properties. Propositional and predicate logic. CTL temporal logic and Kripke structure.
  3. Model checking critical software modules using NuSMV system. CTL temporal logic in requirements specification. 1. homework.
  4. LTL and CTL* temporal logics. Fix point theory in explicit state calculation. Algorithms for state calculation of EX, EG and EU temporal formulas.
  5. Java PathFinder tool for model checking of Java programs. Checking common properties and finding errors in Java programs. 2. homework.
  6. Formal verification of hardware. Overview of methods and tools. Verilog language and VIS tool that is used for formal verification of hardware. Model checking using several examples in VIS.
  7. JML language for annotation and formal verification of Java programs. Symbolic state calculation. Preparation for mid-term exam.
  8. Midterm exam
  9. Formal verification of communication protocols (modeling with Promela language and application of Spin tool) - 1.
  10. Formal verification of communication protocols (modeling with Promela language and application of Spin tool) - 2.
  11. Formal verification of communication protocols (modeling with Promela language and application of Spin tool) - 3. Exposition of typical examples and introduction to homework no. 3.
  12. Construction of reduced ordered binary decision diagrams (ROBDD). ITE algorithm and ROBDD implementation. Application of ROBDDs in model checking.
  13. Algorithms for solving Boolean formula satisfiability problem (SAT-problem). DPLL, GRASP, Chaff and MiniSAT methods. Application in bounded model checking.
  14. Symbolic program execution. SMT-solvers. Application of SMT-solvers in formal verification of programs. Combining symbolic and concrete program execution for efficient program fault detection.
  15. Final exam

Study Programmes

University graduate
Computer Engineering (profile)
Theoretical Course (2. semester)
Computer Science (profile)
Theoretical Course (2. semester)
Information Processing (profile)
Theoretical Course (2. semester)
Software Engineering and Information Systems (profile)
Theoretical Course (2. semester)
Telecommunication and Informatics (profile)
Theoretical Course (2. semester)

Literature

Michael Huth, Mark Ryan (2004.), Logic in Computer Science, Cambridge University Press
B.Berard, M.Bidoit, A.Finkel, F.Laroussinie, A.Petit, L.Petrucci, Ph.Schnoebelen, P.McKenzie (2001.), Systems and Software Verification, Springer-Verlag
Klaus Schneider (2010.), Verification of Reactive Systems: Formal Methods and Algorithms, Springer-Verlag

General

ID 34401
  Summer semester
5 ECTS
L1 English Level
L1 e-Learning
45 Lectures
0 Exercises
0 Laboratory exercises
0 Project laboratory

Grading System

88 Excellent
73 Very Good
58 Good
50 Acceptable