Formal Methods in System Design
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.
- define and state the notion of correct system execution.
- distinguish between correct and incorretc system bahavior.
- apply formal logic in expressing (desired) system behavior.
- analyze and classify the output of tool for formal system verification..
- modify the system structure in order to satisfy the desired behavior.
- design and integrate or modify tools for formal system verification.
- construct formal models of real systems suitable for verification.
Forms of Teaching
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
|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
- 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.
- The role of mathematical logic in specifying and verifying structural and behavioral system properties. Propositional and predicate logic. CTL temporal logic and Kripke structure.
- Model checking critical software modules using NuSMV system. CTL temporal logic in requirements specification. 1. homework.
- LTL and CTL* temporal logics. Fix point theory in explicit state calculation. Algorithms for state calculation of EX, EG and EU temporal formulas.
- Java PathFinder tool for model checking of Java programs. Checking common properties and finding errors in Java programs. 2. homework.
- 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.
- JML language for annotation and formal verification of Java programs. Symbolic state calculation. Preparation for mid-term exam.
- Midterm exam
- Formal verification of communication protocols (modeling with Promela language and application of Spin tool) - 1.
- Formal verification of communication protocols (modeling with Promela language and application of Spin tool) - 2.
- 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.
- Construction of reduced ordered binary decision diagrams (ROBDD). ITE algorithm and ROBDD implementation. Application of ROBDDs in model checking.
- Algorithms for solving Boolean formula satisfiability problem (SAT-problem). DPLL, GRASP, Chaff and MiniSAT methods. Application in bounded model checking.
- 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.
- Final exam