Formal Methods for Verification and Synthesis of Software Systems

Data is displayed for the academic year: 2024./2025.

Lecturers

Asst. Prof.
Frano Škopljanac-Mačina
PhD

Course Description

The role of specification and verification during software system development. The advantages and disadvantages of applying formal methods. Theory and practice during the development of software systems. Formal approaches to modelling software systems. Theoretical background: process algebras, Petri nets and temporal logic. The difference between model checking, testing and run-time verification. Formal communication models. Practical application of specification, verification and testing languages. Model checking tools as well as software testing tools. Testing automatization. Procedures of automata based programming for rigid and robust software development. The application of inductive synthesis for process mining: proces discovery, process conformance testing and process repair. Aplication to business proces mining and specification mining.

Study Programmes

University graduate
[FER3-EN] Control Systems and Robotics - profile
Elective courses (1. semester)
[FER3-EN] Data Science - profile
Elective Courses (3. semester)
[FER3-EN] Electrical Power Engineering - profile
Elective courses (1. semester) (3. semester)

Learning Outcomes

  1. analyse the problem domain
  2. create usable (formal) model that describe the problem
  3. identify method(s) to find the solution
  4. analyse the model: Is model describing problem in a usable way?
  5. derive problem solution
  6. compare results with other similar approaches
  7. revise solution if results are not satisfactory

Forms of Teaching

Lectures

Before each lecture lecture notes and presentations are on course web page

Seminars 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 laboratory

Laboratory

complex laboratory assignments which includes: model checking tool application on selected examples, rigid software development

Grading Method

Continuous Assessment Exam
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

  1. Role of formal specification and analysis techniques in the software development cycle for concurrent reactive systems. Rigid and robust software development.
  2. Formal program and software system modeling: process algebras, Petri nets and finite discrete automaton
  3. Formal model driven software development: specification, testing and verification languages. Model and communicating processes semantic.
  4. Temporal logic, program and software system models. Behavior equivalence.
  5. Verification: Spin model checker and Promela language
  6. Verification: model checking and Petri nets
  7. Software model checking
  8. Midterm exam
  9. Program and software system synthesis: from verified specification to target code skeleton
  10. Inductive synthesis and process mining: process discovery and specification mining
  11. Process mining: conformance testing and process repair
  12. Automatized software testing with model checkers. Runtime verification
  13. New trends for rigid and robust software development. Conections beetwen artificial inteligence and software design.
  14. Project
  15. Final exam

Literature

Edmund M. Clarke, Orna Grumberg, Doron A. Peled (2000.), Model Checking, MIT Press
Mordechai Ben-Ari (2012.), Mathematical Logic for Computer Science, Springer Publishing Company
G. Holzman (2011.), The Spin Model Checker, Addison-Wesley Professional
Paul Ammann, Jeff Offutt (2016.), Introduction to Software Testing, Cambridge University Press
Peterson, J.L. (1981.), Petri Net Theory and the Modeling of Systems, Prentice Hall PTR
Manfred Broy et all (2005.), Model-Based Testing of Reactive Systems, Springer
Mark Utting Bruno Legeard: (2006.), Practical Model-based Testing: a Tools Approach, Morgan Kaufmann
C.A.R. Hoare (2015.), Communicating Sequential Procceses, Prentice-Hall
(.), razni članci iz časopisa i konferencijski zbornici koji će tek biti objavljeni,
Wil van der Aalst (2016.), Process Mining: Data Science in Action, Springer

General

ID 222962
  Winter semester
5 ECTS
L3 English Level
L2 e-Learning
30 Lectures
0 Seminar
0 Exercises
15 Laboratory exercises
0 Project laboratory
0 Physical education excercises

Grading System

90 Excellent
75 Very Good
60 Good
50 Sufficient

Similar Courses