Formalne metode u oblikovanju sustava

Prijava

HrvatskihrEnglishen

Pristupačnost

Veličina slova:A A

Izgled stranice Uobičajen izgled Jednostavni izgled stranice

Kontrast stranice: Normalno Visoki kontrast Inverzni visoki kontrast

Očisti sve

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

definirati i navesti pojam ispravnog rada sustava.
razlikovati pogrešno i ispravno ponašanje sustava.
primijeniti formalnu logiku u opisu (željenog) ponašanja sustava.
analizirati i klasificirati odziv alata za formalnu verifikaciju sustava.
modificirati strukturu sustava kako bi se zadovoljilo željeno ponašanje.
dizajnirati i integrirati ili modificirati alate za formalnu verifikaciju sustava.
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	Prag	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

Administracija predmeta, primjeri pogrešaka u oblikovanju sustava. Motivacija za stjecanje znanja iz formalnih metoda u postupku oblikovanja. Klasifikacija postupaka formalne verifikacije sustava.
Uloga matematičke logike u specifikaciji i provjeri zahtjeva na ponašanje sustava. Propozicijska i predikatna logika. Vremenska logika CTL i Kripkeova struktura.
Provjera modela kritičnih programskih dijelova korištenjem sustava NuSMV. CTL vremenska logika u specifikaciji zahtjeva sustava. 1. domaća zadaća.
Vremenske logike LTL i CTL*. Teorija fiksne točke kod eksplicitnog izračunavanja skupova stanja. Algoritmi izračunavanja skupova stanja za vremenske formule EX, EG i EU.
Alat Java PathFinder za provjeru modela programa pisanih u programskom jeziku Java. Provjera čestih svojstava i pronalaženje pogrešaka u programima pisanima u Javi. 2. domaća zadaća.
Formalna verifikacija sklopovlja. Pregled metoda i alata. Jezik Verilog i alat VIS koji se koristi za formalnu verifikaciju sklopovlja. Provjera modela u VIS-u na nekoliko primjera.
Jezik JML za označavanje i formalnu verifikaciju Javinih programa. Simboličko izračunavanje skupova stanja. Priprema za međuispit.
Provjera znanja
Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 1.
Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 2.
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.
Izgradnja reduciranih uređenih binarnih dijagrama odlučivanja (ROBDD). Algoritam ITE i implementacija ROBDD-a. Primjena ROBDD-a u provjeri modela.
Algoritmi za rješavanja problema zadovoljivosti skupa Booleovih formula (SAT-problem). Postupci DPLL, GRASP, Chaff i MiniSAT. Primjena u ograničenoj provjeri modela.
Simboličko izvršavanje programa. SMT-rješavači. Primjena SMT-rješavača u formalnoj verifikaciji programa. Kombiniranje simboličkog i konkretnog izvršavanja programa radi učinkovitog pronalaska pogrešaka u programima.
Završna provjera znanja