Formal Methods for Verification and Synthesis of Software Systems
- analyse the problem domain
- create usable (formal) model that describe the problem
- identify method(s) to find the solution
- analyse the model: Is model describing problem in a usable way?
- derive problem solution
- compare results with other similar approaches
- revise solution if results are not satisfactory
Forms of Teaching
Before each lecture lecture notes and presentations are on course web pageSeminars and workshops
the application of formal methods on rigid software development ("design-for-verification" and "correct-by-construction" systems)Independent assignments
homework assignments, preparation for work in laboratoryLaboratory
complex laboratory assignments which includes: model checking tool application on selected examples, rigid software development
|Type||Threshold||Percent of Grade||Threshold||Percent of Grade|
|Laboratory Exercises||0 %||20 %||0 %||20 %|
|Homeworks||0 %||15 %||0 %||15 %|
|Seminar/Project||0 %||10 %||0 %||10 %|
|Mid Term Exam: Written||0 %||30 %||0 %|
|Final Exam: Written||0 %||35 %|
|Exam: Written||0 %||65 %|
Week by Week Schedule
- Role of formal specification and analysis techniques in the software development cycle for concurrent reactive systems. Rigid and robust software development.
- Formal program and software system modeling: process algebras, Petri nets and finite discrete automaton
- Formal model driven software development: specification, testing and verification languages. Model and communicating processes semantic.
- Temporal logic, program and software system models. Behavior equivalence.
- Verification: Spin model checker and Promela language
- Verification: model checking and Petri nets
- Software model checking
- Midterm exam
- Program and software system synthesis: from verified specification to target code skeleton
- Inductive synthesis and process mining: process discovery and specification mining
- Process mining: conformance testing and process repair
- Automatized software testing with model checkers. Runtime verification
- New trends for rigid and robust software development. Conections beetwen artificial inteligence and software design.
- Final exam