Rozdíly

Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.

--- courses:a4m33tvs:okruhy [2015/01/08 20:29]
koprija6 [(a) Princip a základní charakteristiky metod ověřování modelů.]
+++ courses:a4m33tvs:okruhy [2025/01/03 18:29] (aktuální)
@@ Řádek 401: / Řádek 401: @@
   - kazdy prechod
-=====6. Statistické testování softwaru=====
+=====6. Ověřování modelu=====
-====(a) Propagace kovarianční matice - explicitní vztah.====
-Explicitní vztah: Y = F(X)
-  * X .. vstup
-  * Y .. výstup
-Jak se počítá kovarianční matice pro parametr p:
-  - vyjádří se p
-  - J je matice 1x2: derivace p podle x a derivace p podle y
-  - kovarianční matice se počítá: J x matice 2x2 viz úkol x transponovaná J
-====(b) Propagace kovarianční matice - implicitní vztah.====
-Implicitní vztah: skalární funkce F(X,Y)
-====(c) Přímé propagování variance.====
-Dána funkce g(x,y) s variancí (delta_xx)^2 a (delta_yy)^2 a kovariancí delta_xy.
-Příklad pro z = x + y:
-(delta_zz)^2 = (delta_xx)^2 + (delta_yy)^2
-====(d) Přímé propagování min/max chyby.====
-=====7. Ověřování modelu=====
 ====(a) Princip a základní charakteristiky metod ověřování modelů.====
 == Temporální verifikace modelů==
@@ Řádek 438: / Řádek 416: @@
   * úplná automatizace,
   * vysoká rychlost,
-  * možnost verikace i částečných specifikací,
+  * možnost verifikace i částečných specifikací,
   * produkuje protipříklady.
 Nevýhody
@@ Řádek 554: / Řádek 532: @@
   * clocks, clock differences, integer variables and constants
-=====8. Temporální logiky=====
+=====7. Temporální logiky=====
 ====(a) Cesta výpočtu a pojem času.====
   * Abstrakce času
@@ Řádek 605: / Řádek 583: @@
-=====9. Formální metody=====
+=====8. Formální metody=====
 ====(a) Z notace - principy a základní vlastnosti.====
-- je jedna ze standartizovanych notaci
+  * je jedna ze standartizovanych notaci
-- Z je prave jenom notace
+    * Z je prave jenom notace
-  -> neni exekucni
+    * neni exekucni
-  -> neni to programovaci jazyk
+    * neni to programovaci jazyk
-- je zalozena na teorii mnozin a matematicke logice
+  * Z notace je zalozena na:
-Matematickou logikou je predikatovy kalkulus prveho radu.
+    * teorii mnozin
-Z je zalozena na modelech. System je modelovan pomoci:
+    * matematicke logice (predikatovy kalkulus prveho radu)
- - stavu (na zaklade stavovych promennych a jejich hodnot)
+    * na modelech
- - operaci, ktere mohou menit stav
+  * System je modelovan pomoci:
+    * stavu (na zaklade stavovych promennych a jejich hodnot)
+    * operaci, ktere mohou menit stav
 Schema = vzory deklaraci a omezeni
@@ Řádek 640: / Řádek 620: @@
   - typova kontrola
   - dokazovani
+  -
+====(c) Alloy - prvky syntaxe jazyka, signatura, pole, relace, množinové operátory, relační operátory, fakta, funkce, predikáty, tvrzení, jak se provádí analýza specifikace.====
+https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/05.alloy.pdf
+**atom** je primitivni entita
+  * nedelitelna
+  * nemenna
+  * neinterpretovana (nema zadnou vestavenou vlastnost)
+**relace** je struktura, ktera zachycuje vztahy mezi atomy. je to mnozina n-tic, kazda n-tice je sekvence atomu
+**signatura** zavadi mnozinu atomu, je vrcholova pokud je deklarovana nezavisle na ostatnich signaturach
+  * deklarace: sig A {}
+  * rozsireni: sig A1 extends A {}
+  * podmnozina: sig A1 in A {}
+  * abstraktni (nema zadne elementy): abstract sig A {}
+**pole**, relace se deklaruji jako pole v signature:
+  * sig A { f: e} ... domena A, obraz e
+  * sig A { f1: A} ... binarnirelace, f1 je podmnozinou A x A
+  * sig B { f2: A -> A } .. ternarni relace, f2 je podmnozinou B x A x A
+**nasobnosti**
+  * signatury: m sig A { f: e}
+  * poli: sig A { f:  m e}, sig A { f: e1 m -> n e2}
+  * mozne nasobnosti (m, n):
+    * set: jakykoli pocet
+    * some: jeden a vice
+    * lone: nula nebo jeden
+    * one: presne jeden
+**kvantifikatory:** all, some, no, lone, one
+**logicke operatory:** not (!), and (&&), or (||), implies (=>), else, (<=>)
+**množinové konstanty**
+  * none: prazdna mnozina
+  * univ: univerzalni mnozina
+  * ident: identita
+**množinové operátory**
+  * + : sjednoceni
+  * & : prunik
+  * - : rozdil
+  * in : podmnozina
+  * = : rovnost
+**relační operátory**
+  * -> sipka (soucin) ... konkatenace
+  * ~ transpozice ... zrcadlovy obraz
+  * . dot join
+    * {(a,b)}.{(a,c)} = {}
+    * {(a,b)}.{(b,c)} = {(a,c)}
+    * {(a)}.{(a)} = nedefinovano !! je definovano, tehdy a jen tehdy, jestlize obe nejsou unarni relace !!
+    * p a q
+      * jsou dve relace a nejsou obe unarni
+      * p.q je relace, ktera vznikne kombinaci vsech n-tic z p a m-tic z q a pridanim jejich spojeni, pokud tento existuje.
+  * [] box join ... p[q] == q.p
+  * ^ tranzitivni uzaver ... ^r = r + r.r + r.r.r + ...
+  * * reflexivne-tranzitivni uzaver ... *r = ^r + iden
+  * <: omezeni domeny
+  * :> omezeni obrazu
+  * ++ prepsani
+**fakta** jsou dalsi omezeni na signatury
+  * fact selfAncestor { no p: Person | p in p.^parents }
+**funkce** (makra) jsou pojmenovane vyrazy
+  * 0 a vice argumentu
+  * navratova hodnota je vyraz
+  * vyvolavaji se pouze, pokud je na ne odkazovano
+  * fun sisters [p: Person]: { { w: Woman | w in p.siblings } }
+**predikáty** jsou dobre v situacich:
+  * omezeni, ktera nechceme zaznamenat jako fakta
+  * omezeni, ktera chceme pouzivat vicekrat
+  * vyvolavaji se pouze, pokud ne na ne odkazovano
+  * pred BloodRelated [p: Person, q: Person] { some p.*parents & q.*parents }
+**tvrzení** slouzi jako dodatecna omezeni k overeni. Neni-li omezeni vyjadrene tvrzenim splneno, vyprodukuje se protipriklad.
+**jak se provádí analýza specifikace**
+  * prikazem **run** (pouze prvni prikaz v souboru) se pusti analyza modelu, tzn. hledej instance modelu
+  * hleda se pouze v omezenem prostoru instanci urcenem rozsahem
+    * run {} .. prednastaveny rozsah 3
+    * run {} for 5 ... rozsah 5
+    * run { some Man && no Married } ... s podminkami
+=====9. JPF=====
+====(a) Architektura systemu JPF a vlastnosti systemu.====
+slidy(pdf strany) 30-37
+https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/11.javapathfinder.pdf
+====(b) Pouziti systemu JPF pro generovani testovacich pripadu.====
+slidy(pdf strany) 19-28
+https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/11.javapathfinder.pdf
 =====10. testování OO softwaru=====
 ====(a) Anomálie DU párů====
@@ Řádek 647: / Řádek 725: @@
 Souvisi to s dedenim a polymorfismem.
-  - SDA - state definition anomaly - přepisící metoda má jinou def množinu než přepisovaná
+  - SDA - state definition anomaly - přepisující metoda má jinou def množinu než přepisovaná
   - ITU - inconsistent type use - nepřepisování ale volání parent metod
   - SDIH - podobné SDA ale potomek přepíše něco v prarodiči a rodič pak používá špatně definovanou proměnnou
@@ Řádek 703: / Řádek 781: @@
 Behem tohoto testovani po fazi vyvoje, kdy se objevuji selhani, identifikuji a opravuji defekty, se softwarovy produkt stava stabilnejsi a jeho spolehlivost roste s casem. Tyto modely se proto nazyvaji modely rustu spolehlivosti.
-=====12. JPF=====
+=====12. Statistické testování softwaru=====
+====(a) Propagace kovarianční matice - explicitní vztah.====
+Explicitní vztah: Y = F(X)
+  * X .. vstup
+  * Y .. výstup
-====(a) Architektura systemu JPF a vlastnosti systemu.====
+Jak se počítá kovarianční matice pro parametr p:
-====(b) Pouziti systemu JPF pro generovani testovacich pripadu.====
+  - vyjádří se p
+  - J je matice 1x2: derivace p podle x a derivace p podle y
+  - kovarianční matice se počítá: J x matice 2x2 viz úkol x transponovaná J
+====(b) Propagace kovarianční matice - implicitní vztah.====
+Implicitní vztah: skalární funkce F(X,Y)
+====(c) Přímé propagování variance.====
+Dána funkce g(x,y) s variancí (delta_xx)^2 a (delta_yy)^2 a kovariancí delta_xy.
+Příklad pro z = x + y:
+(delta_zz)^2 = (delta_xx)^2 + (delta_yy)^2
+====(d) Přímé propagování min/max chyby.====
+slidy(pdf strany) 19-21
+https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/13.statisticketestovani.pdf
 ~~DISCUSSION~~

courses/a4m33tvs/okruhy.1420745367.txt.gz · Poslední úprava: 2025/01/03 18:24 (upraveno mimo DokuWiki)

Nahoru