Predavanje 11

Question 1

Formalne metode - definicija

Answer 1

Formalne metode u životnom ciklusu razvoja progrmaske potpore obuhvaćaju metode i tehnike zasnovane na matematici i formalnoj logici za oblikovanje složenih sustava

Question 2

Ciljevi formalnih metoda

Answer 2

• izgraditi sustav bez pogrešaka
• pokazati da sustav zadovoljava zahtjeve na ispravan način
• pronaći pogreške u postojećem sustavu
• pokazati da u postojećem sustavu nema pogrešaka

Question 3

Svojstva formalne semantike

Answer 3

1. matematička osnova omogućava precizan opis svojstava
2. jednoznačnost
3. omogućava konzistentnost, ispravnost, te izražavanje specifikacije i implementacije

Question 4

Klasifikacija formalnih metoda

Answer 4

• specifikacija
• sinteza
• verifikacija

Question 5

Formalna verifikacija - definicija

Answer 5

Proces kojim dokazujemo da implementacija sustava posjeduje svojstva i ponašanje kao i formalna specifikacija sustava

Question 6

Metode formalne verifikacije

Answer 6

• dokazivanje teorema
• provjera modela
• provjera ekvivalentnosti

Question 7

Od čega se sastoji proces formalne verifikacije

Answer 7

• odabir ključnog dijela implementacije koja se želi FV
• odabir konkretne formalne metode s pomoću koje se treba provesti FV
• primjena korištene metode FV
• vrednovanje rezultata
• dokumentiranje i ispravljanje nedostataka

Question 8

SAT problem

Answer 8

Tražimo model skupa formula

Question 9

Kripke struktura (S,R,L)

Answer 9

skup stanja S
relacija R
funkcija označavanja L - istiniti atomički simboli u svakom stanju

Question 10

Temeljna postavka izvođenja stroja stanja kao kontekst vremenske logike

Answer 10

Promatramo izvođenje stroja stanja kroz sve moguće putove

Question 11

Kvantifikator A

Answer 11

All, istražujemo sve putove izvođenja počevši od nekog stanja

Question 12

Kvantifikator E

Answer 12

Exists, postoji najmanje jedanput na kojem je svojstvo zadovoljeno

Question 13

Vremenski operator X

Answer 13

Neposredni sljedbenici ili sljedbenik

Question 14

Vremenski operator G

Answer 14

Provjeravaju se sva stanja

Question 15

Vremenski operator F

Answer 15

Provjeravaju se neka moguća dosegnuta ili dosegnuto

Question 16

Vremenski operator U

Answer 16

Provjerava se da li su atomički simboli istiniti u stanjima duž puta ili putova dok se ne stigne u stanje koje nas zanima

Question 17

Posebnost “Until” (A U B)

Answer 17

• A može biti istinit ili ne u i nakon stanja u kojem je B = true
• B može biti istinit i prije početnog stanja s

Question 18

Hoareovo pravilo

Answer 18

Za ispravan rad programa C vrijedi: “Ako je istinit preduvjet prije
izvođenja C, tada završni uvjet mora biti istinit završetkom izvođenja C.”