Courses – Fakultet tehničkih nauka u Novom Sadu

Subject: Formal Methods for Modelling of Software Systems (17.IFE256)

Native organizations units: Chair of Applied Computer Science

Type of studies	Title
Master Academic Studies	Information and Analytics Engineering (Year: 1, Semester: Summer)
Master Academic Studies	Information Engineering (Year: 1, Semester: Summer)

General information:

Category	Scientific-professional
Scientific or art field	Applied Computer Science and Informatics
ECTS	6

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.

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.

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 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.

Authors	Title	Year	Publisher	Language
R. D. Tennent	Specifying Software: A Hands-On Introduction	2002	Cambridge University Press	English
J. M. Spivey	The Z Notation: A Reference Manual	1992	Prentice Hall	English
Michael Huth, Mark Ryan	Logic in Computer Science: Modelling and Reasoning about Systems	2004	Cambridge University Press	English