Formalne metode u oblikovanju sustava

Opis predmeta

Matematički zasnovani postupci specifikacije, razvoja i verifikacije sklopovskih i programskih sustava s ciljem poboljšanja kvalitete završnog proizvoda uz istovremeno smanjivanje vremena stavljanja proizvoda na tržište. Matematička logika kao temelj specifikacijskih jezika. Dedukcijski sustavi. Oblici formalnih specifikacijskih jezika. Modeli izvedbe sklopovskih i programskih sustava. Specifikacija i verifikacija izračunskih i reaktivnih sustava. Postupci verifikacije dokazivanjem teorema i provjerom modela. Alati za automatiziranu formalnu verifikaciju sustava. Formalno koncepcijsko modeliranje. Primjene u različitim domenama računalnog sklopovskog i programskog inženjerstva.

Opće kompetencije

Studenti ovladavaju znanjima o realnim dosezima i uporabi formalnih metoda u oblikovanju sustava. Posebice se stiču znanja o izgradnji modela ciljnog sustava, te postupcima zadovoljavanja specificiranih strukturnih i funkcijskih zahtjeva.

Ishodi učenja

  1. definirati i navesti pojam ispravnog rada sustava.
  2. razlikovati pogrešno i ispravno ponašanje sustava.
  3. primijeniti formalnu logiku u opisu (željenog) ponašanja sustava.
  4. analizirati i klasificirati odziv alata za formalnu verifikaciju sustava.
  5. modificirati strukturu sustava kako bi se zadovoljilo željeno ponašanje.
  6. dizajnirati i integrirati ili modificirati alate za formalnu verifikaciju sustava.
  7. kreirati formalne modele realnih sustava pogodne za verifikaciju.

Oblici nastave

Predavanja

Nasatava je organizirana kroz dva ciklusa. Prvi ciklus sastoji se od 7 tjedana predavanja i međuispita. Drugi ciklus sastoji se iz 6 tjedna predavanja i završnog ispita.

Provjere znanja

Kratke provjere (3), domaće zadaće (3), međuispit, završni ispit.

Način ocjenjivanja

Kontinuirana nastava Ispitni rok
Vrsta provjere Prag Udio u ocjeni Napomena / komentar Udio u ocjeni
Domaće zadaće 0 % 30 % 0 % 30 %
Kratke provjere znanja 0 % 9 % 0 % 9 %
Međuispit: Pismeni 0 % 25 % 0 %
Završni ispit: Pismeni 0 % 36 %
Ispit: Pismeni 0 % 61 %

Tjedni plan nastave

  1. Administracija predmeta, primjeri pogrešaka u oblikovanju sustava. Motivacija za stjecanje znanja iz formalnih metoda u postupku oblikovanja. Klasifikacija postupaka formalne verifikacije sustava.
  2. Uloga matematičke logike u specifikaciji i provjeri zahtjeva na ponašanje sustava. Propozicijska i predikatna logika.
  3. CTL vremenska logika za opis ponašanja sustava. Kripke struktura. Metoda provjere modela u formalnoj verifikaciji sustava.
  4. Verilog jezik za opis i modeliranje sklopovlja. Primjeri opisa kombinacijskih i sekvencijskih sklopova.
  5. VIS alat za formalnu verifikaciju sklopovlja. Preslikavanje Verilog opisa sklopovlja u interni VIS opis. Prikaz primjera verifikacije i uvod u domaću zadaću br. 1 (verifikacija arbitra sabirnice).
  6. LTL vremenska logika za opis ponašanja sustava. Uvod u formalne metode za verifikaciju programskih produkata. Metoda ograničene provjere modela za C programe. Alloy alat za opis sustava i verifikaciju logičkih tvrdnji.
  7. Modeliranje sustava NuSMV alatom. Opis jezika i upravljačkih konstrukcija. Prikaz primjera i uvod u zadatke za domaću zadaću br. 2 (verifikacija protokola međusobnog isključivanja).
  8. Provjera znanja
  9. Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 1.
  10. Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 2.
  11. Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 3. Prikaz primjera i uvod u zadatke za domaću zadaću br. 3.
  12. Eksplicitni postupci izračunavanja u formalnoj verifikaciji sustava. Pojam čvrste točke i algoritmi izračunavanja vremenskih formula EX, EG, EU.
  13. Simboličko predstavljanje matematičkih objekata i izgradnja reducuranih uređenih binarnih dijagrama odlučivanja (ROBDD).
  14. Primjena reduciranih uređenih binarnih dijagrama odlučivanja (ROBDD) u formalnoj verifikaciji sustava.
  15. Završna provjera znanja

Studijski programi

Sveučilišni diplomski
Obradba informacija (profil)
Teorijski predmeti profila (2. semestar)
Programsko inženjerstvo i informacijski sustavi (profil)
Teorijski predmeti profila (2. semestar)
Računalno inženjerstvo (profil)
Teorijski predmeti profila (2. semestar)
Računarska znanost (profil)
Teorijski predmeti profila (2. semestar)
Telekomunikacije i informatika (profil)
Teorijski predmeti profila (2. semestar)

Literatura

Michael Huth, Mark Ryan (2004.), Logic in Computer Science, Cambridge University Press
B.Berard, M.Bidoit, A.Finkel, F.Laroussinie, A.Petit, L.Petrucci, Ph.Schnoebelen, P.McKenzie (2001.), Systems and Software Verification, Springer-Verlag
Klaus Schneider (2010.), Verification of Reactive Systems: Formal Methods and Algorithms, Springer-Verlag

Predavanja

Izvedba

ID 34401
  Ljetni semestar
5 ECTS
R1 Engleski jezik
R1 E-učenje
45 Predavanja
0 Auditorne vježbe
0 Laboratorijske vježbe

Ocjenjivanje

88 izvrstan
73 vrlo dobar
58 dobar
50 dovoljan