Formalne metode za verifikaciju i sintezu programskih sustava

Prikazani su podaci za akademsku godinu: 2022./2023.

Nositelji

Izv. prof. dr. sc.
Bruno Blašković

Opis predmeta

Formalna specifikacija i verifikacija tijekom razvoja programskih sustava. Prednosti i mane primjene formalnih metoda. Primjena teorije i prakse tijekom razvoja programskih sustava. Formalni pristupi za modeliranje programske potpore. Teorijska podloga: procesne algebre, Petrijeve mreže i temporalna logika. Razlika između provjere modela, testiranja i verifikacije reaktivnih konkurentnih sustava.. Formalni model komunikacije među procesima. Praktična primjena jezika za specifikaciju, testiranje i verifikaciju. Alati za provjeru modela i alati za testiranje programske potpore. Postupci automatizacije testiranja. Postupci razvoja programa utemeljeni na automatima za razvoj rigidne i robusne programske potpore. Induktivna sinteza za dubinsku analizu procesa: otkrivanje procesa, analiza svojstava procesa i popravak procesa. Primjena na dubinsku analizu poslovnih procesa i specifikacije programskih sustava.

Studijski programi

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

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

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
R1 Engleski jezik
R2 E-učenje
30 Predavanja
0 Seminar
0 Auditorne vježbe
15 Laboratorijske vježbe
0 Konstrukcijske vježbe

Ocjenjivanje

90 izvrstan
75 vrlo dobar
60 dobar
50 dovoljan

Sličan predmet