Formalne metode za verifikaciju i sintezu programskih sustava

Ishodi učenja

  1. analizirati domenu problema
  2. kreirati upotrebljiv (formalni) model problema
  3. identificirati metodu, postupke, algoritme za pronalaženje rješenja
  4. analizirati model: Da li model opisuje problem na upotrebljiv način?
  5. prikazati rješenje problema
  6. staviti rješenje u odnos sa sličnim rješenjima
  7. preurediti rješenje ako rezultati ne zadovoljavaju

Oblici nastave

Predavanja

materijali i prezentacije unaprijed stavljene na web-stranicu predmeta

Seminari i radionice

primjena formalnih metoda na razvoj rigidne programske potpore (oblikovanje za verifikaciju i "correct-by-construction" program)

Samostalni zadaci

domaće zadaće, priprema za laboratorijske vježbe

Laboratorij

složeni laboratorijski zadaci koji obuhvaćaju: provjeru modela primjenom alata, rad na razvoju rigidne programske potpore

Način ocjenjivanja

Kontinuirana nastava Ispitni rok
Vrsta provjere Prag Udio u ocjeni Prag Udio u ocjeni
Laboratorijske vježbe 0 % 20 % 0 % 20 %
Domaće zadaće 0 % 15 % 0 % 15 %
Seminar/Projekt 0 % 10 % 0 % 10 %
Međuispit: Pismeni 0 % 30 % 0 %
Završni ispit: Pismeni 0 % 35 %
Ispit: Pismeni 0 % 65 %

Tjedni plan nastave

  1. Uloga tehnika formalne specifikacije i verifikacije u životnom ciklusu programske potpore za konkurentne reaktivne sustave. Rigidni i robustni razvoj programske potpore.
  2. Modeliranje programa i programskih sustava: procesne algebre, Petrijeva mreža, konačni diskretni automati
  3. Razvoj programske potpore utemeljen na modelima: specifikacijski jezici, jezici za ispitivanje i jezici za verifikaciju. Semantika modela i komunicirajućih procesa.
  4. Temporalne logike, modeli programa i programskih sustava. Jednakosti ponašanja.
  5. Verifikacija: programski alat Spin i jezik Promela
  6. Verifikacija: provjera modela i Petrijeve mreže
  7. Statička analiza programa provjerom modela
  8. Međuispit
  9. Sinteza programa i programskih sustava transformacijom specifikacije u ciljanu programsku strukturu
  10. Induktivna sinteza i dubinska analizi procesa: otkrivanje modela i specifikacije procesa
  11. Dubinska analiza procesa: testiranje i popravljanje svojstava dobivenog modela
  12. Automatizirano testiranje programske potpore provjerom modela. Verifikacija programske potpore tijekom izvođenja.
  13. Novi trendovi za rigidni i robustni razvoj programske potpore. Veza umjetne inteligencije i oblikovanja programske potpore.
  14. Projekt
  15. Završni ispit

Studijski programi

Sveučilišni diplomski
Audiotehnologije i elektroakustika (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Automatika i robotika (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Elektroenergetika (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Elektroničko i računalno inženjerstvo (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Elektronika (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Elektrostrojarstvo i automatizacija (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Informacijsko i komunikacijsko inženjerstvo (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Komunikacijske i svemirske tehnologije (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Programsko inženjerstvo i informacijski sustavi (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Računalno inženjerstvo (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Računalno modeliranje u inženjerstvu (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)
Računarska znanost (profil)
Slobodni izborni predmeti (3. semestar) Slobodni zborni predmeti (1. semestar)
Znanost o mrežama (profil)
Izborni predmeti profila (3. semestar)
Znanost o podacima (profil)
Slobodni izborni predmeti (1. semestar) (3. semestar)

Literatura

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

Za studente

Izvedba

ID 222520
  Zimski semestar
5 ECTS
R3 Engleski jezik
R2 E-učenje
30 Predavanja
15 Laboratorijske vježbe

Ocjenjivanje

90 izvrstan
75 vrlo dobar
60 dobar
50 dovoljan