Subject: Formal Methods for Modelling of Software Systems (17.IFE256 )
Native organizations units: Chair of Applied Computer Science
Study programmes of the course:
| Type of studies | Title |
|---|---|
| Master Academic Studies | Information Engineering (Godina: 1, Summer) |
| Master Academic Studies | Information and Analytics Engineering (Godina: 1, Summer) |
Educational goal:
Education of students in the area of formal methods for software system modeling and systems in which the software is applied. Adopting approaches and application techniques of formal methods for software system modeling and systems in which the software is applied.
Educational outcome:
By the end of the course, students should be able to: • Use mathematical structures such as sets, bags, functions and relations to formally specify software systems, and to state desired properties of such systems. • Check their formal specification, model checking and proving some properties of the software system specification. • Use mathematical reasoning to prove simple properties of software models. • Create model transformation specifications, create program code generators and in simple cases produce verified refinements of their specifications.
Course content:
Introduction to Formal Methods. Z notation. Hoare Logic and Program Verification. Hoare triples. Partial and total correctness. A proof calculus for partial correctness. Weakest preconditions and automatic verification. Temporal Logic and other logic types application in system modeling and and model checking. Linear-time Temporal Logic. Model checking based on an automata based approach. Model checking based on LTL.
Teaching methods:
Teaching is performed through lessons, oral and computer exercises (in the computer classroom), as well as consultations. Through the teaching process, students are constantly motivated to an intensive discussion, problem oriented reasoning, independent study work and active participation in the whole lecturing process. The prerequisite to enter final exam is to complete all the pre-exam assignments by earning at least 30 points.
Literature:
| Authors | Title | Year | Publisher | Language |
|---|---|---|---|---|
| 2002 | English | |||
| 1992 | English | |||
| 2004 | English |
Knowledge evaluation:
| Course activity | Pre-examination | Obligations | Number of points |
|---|---|---|---|
| Oral part of the exam | No | Yes | 30.00 |
| Test | Yes | Yes | 10.00 |
| Project | Yes | Yes | 30.00 |
| Test | Yes | Yes | 10.00 |
| Complex exercises | Yes | Yes | 20.00 |
Lecturers:
vanr. prof. dr Gajić Dušan
Associate Professor
Lectures
Asistent dr Vještica Marko
Assistant - Master
Computational classes
vanr. prof. dr Dimitrieski Vladimir
Associate Professor
Computational classes
vanr. prof. dr Dimitrieski Vladimir
Associate Professor
Lectures
Faculty of Technical Sciences
© 2024. Faculty of Technical Sciences.
Contact:
Address: Trg Dositeja Obradovića 6, 21102 Novi Sad
© 2024. Faculty of Technical Sciences.