Formalne metode za verifikaciju i sintezu programskih sustava
Prikazani su podaci za akademsku godinu: 2024./2025.
Nositelji
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
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)
Izborni predmeti
(1. semestar)
(3. semestar)
[FER3-HR] Elektronika - profil
Izborni predmeti
(1. semestar)
(3. semestar)
Izborni predmeti
(1. semestar)
(3. semestar)
Izborni predmeti
(1. semestar)
(3. semestar)
Izborni predmeti
(1. semestar)
(3. semestar)
Izborni predmeti
(1. semestar)
(3. semestar)
[FER3-HR] Računalno inženjerstvo - profil
Izborni predmeti
(1. semestar)
(3. semestar)
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
- analizirati domenu problema
- kreirati upotrebljiv (formalni) model problema
- identificirati metodu, postupke, algoritme za pronalaženje rješenja
- analizirati model: Da li model opisuje problem na upotrebljiv način?
- prikazati rješenje problema
- usporediti rješenje s drugim sličnim pristupima
- preurediti rješenje ako rezultati ne zadovoljavaju
Oblici nastave
Predavanja
materijali i prezentacije unaprijed stavljene na web-stranicu predmeta
Seminari i radioniceprimjena formalnih metoda na razvoj rigidne programske potpore (oblikovanje za verifikaciju i "correct-by-construction" program)
Samostalni zadacidomaće zadaće, priprema za laboratorijske vježbe
Laboratorijslož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
- Uloga tehnika formalne specifikacije i verifikacije u životnom ciklusu programske potpore za konkurentne reaktivne sustave. Rigidni i robusni razvoj programske potpore.
- Modeliranje programa i programskih sustava: procesne algebre, Petrijeva mreža, konačni diskretni automati
- Razvoj programske potpore utemeljen na modelima: specifikacijski jezici, jezici za ispitivanje i jezici za verifikaciju. Semantika modela i komunicirajućih procesa.
- Temporalne logike, modeli programa i programskih sustava. Jednakosti ponašanja.
- Verifikacija: programski alat Spin i jezik Promela
- Verifikacija: provjera modela i Petrijeve mreže
- Statička analiza programa provjerom modela
- Međuispit
- Sinteza programa i programskih sustava transformacijom specifikacije u ciljanu programsku strukturu
- Induktivna sinteza i dubinska analizi procesa: otkrivanje modela i specifikacije procesa
- Dubinska analiza procesa: testiranje i popravljanje svojstava dobivenog modela
- Automatizirano testiranje programske potpore provjerom modela. Verifikacija programske potpore tijekom izvođenja.
- Novi trendovi za rigidni i robusni razvoj programske potpore. Veza umjetne inteligencije i oblikovanja programske potpore.
- Projekt
- Završni ispit
Literatura
(.), razni članci iz časopisa i konferencijski zbornici koji će tek biti objavljeni,
Izvedba
ID 222520
Zimski semestar
5 ECTS
R2 Engleski jezik
R2 E-učenje
30 Predavanja
0 Seminar
0 Auditorne vježbe
15 Laboratorijske vježbe
0 Konstrukcijske vježbe
0 Vježbe tjelesnog odgoja
Ocjenjivanje
90 izvrstan
75 vrlo dobar
60 dobar
50 dovoljan