Okruhy otázek

• 5 ze 6 softwarových projektů je neúspěšných,
• 1/3 projektů je přerušena,
• projekty předávány za dvojnásobnou cenu než dohodnuto,
• projekty se předávají za dvojnásobně dlouhou dobu než se plánuje.

rozdíl mezi SW a testovací proces
Opakované použití: testovací metodika by neměla být vyvíjena pouze pro jediný projekt.
Flexibilita: vyjádření nových konceptů, návrhových šablon.
Adaptivita: malé modifikace v implementaci softwaru by měly býtpokryty automatizovaně.
Komplexita: pokrytí dostatečné části testovacích případů je často za možnostmi manuální přípravy.
Údržba: potřebné úsilí je nepřímo úměrné exibilitě a adaptivitě, přímo úměrné komplexitě testovaného produktu.
Prezentace stavu: dokumentace pravidelně obnovovaná, např. WWW stránky.
Nástroje: integrovaná řešení adresující výše uvedené položky.
Cena/čas: efektivnost vyjádřená pomocí výše uvedených položek.
Proveditelnost: trh/cena/čas/zdroje/kvalita efektivnost.
Nepřetržitý běh: rychlá odezva, několik fází (zahořovací, . . . , regresní, dokumentace pravidelně obnovovaná)

• nedostatek času - veto na testování
• malé či chybně rozložené náklady - veto na testování,
• chybné nebo chybějící specifikace
• chyby v kódu - nechráněné převody,
• opakované využití - změna specifikací,
• oddělení vývoje softwaru a jeho testování.
• uživatelské rozhraní kontra bezpečnost,
• složitý návrh

• Ariane 5
• Therac 26
• Oběžná dráha Apollo 13: program testován za pomalu se měnících podmínek. Při velké dynamice došlo k vydělení nulou na netestované cestě.
• Mariner let k Venuši: 80 milionů $, záměna za + vedla k odklonu z dráhy,
• Minutí Merkuru: proměnná Fortranu
• Selhání rakety Patriot: během Války v zálivu v 1991 kvůli kumulativní chybě v časové synchronizaci,
• F16 simulace: letadlo se překlápělo při překročení rovníku,
• Návrh jaderné elektrárny: v roce 1979 muselo být 5 jaderných elektráren uzavřeno z důvodu poddimenzování potrubí, velikost vektoru počítána jako součet složek, modul byl napsán studentem na praxi

Reaktivní zabezpečení kvality

• je zaměřeno na detekování a korigování problémů, které již nastaly.
• zdůrazňuje vyhodnocování tradičních ztrát a statistické analýzy nashromážděných pozorování pro podporu akce.
• vede k omezování ztrát.

Proaktivní zabezpečení kvality

• se orientuje na prevenci,
• dává důraz na znalost příčin a následků, riskové analýzy, zkušenosti, zdůvodnění akcí,
• staví na vyšší úrovni spekulace a risku,
• vede k urychlenému vývoji,
• umožňuje vyhnutí se ztrátám

Testování je:

• kontrola programů vzhledem ke specifikacím,
• nalézání chyb v programech,
• určení míry akceptování uživatelem,
• ujištění se o tom, že systém je připraven k používání,
• získání důvěry, že program pracuje,
• prezentace, že program běží správně,
• demonstrace toho, že program je bez chyb,
• porozumění omezení výkonnosti programu,
• učení se toho, co systém není schopen dělat,
• hodnocení schopností programu,
• verifikace dokumentace.

Testování je měření kvality softwaru.

Substitute performance

• based on the developer's own test loads, test environments and test methods
• → performance indices

True product performance

• Customers determine true performance as a result of their field application
• Difficult to measure directly during development, since customers will evaluate performance individually

source: Performance characterization(Google Books)

Kvalita je ztráta, kterou produkt způsobí společnosti po jeho dodání, způsobenou funkčními změnami a škodlivými účinky mimo těch, které vyplývají z vlastních funkcí.

• Funkčnost (externí kvalita)
  • správnost,
  • spolehlivost,
  • použitelnost,
  • integrita.
• Inženýrské řešení (vnitřní kvalita)
  • efektivita,
  • testovatelnost,
  • dokumentace,
  • struktura.
• Adaptabilita (budoucí kvalita)
  • flexibilita,
  • opětné použití,
  • údržba

y . . . produkovaná hodnota výkonnostního indexu,
m . . . hodnota indexu výkonosti požadovaná zákazníkem,
L(y) . . . ztrátová funkce vzhledem k rozdílu mezi y a m,
L(y) může být rozložena do Taylorovy řady okolo m:
L(y) = L(m + y - m) = L(m) + L'(m)/1!(y - m) + L''(m)/2!(y - m)2 + …
za předpokladu L(m) = 0,
L(y) je minimální při y = m, L'(m) = 0,
ztráta může být aproximována: L(y) ~ k(y - m)2
k je neznámý koeficient, k určení k je potřeba vědět ztrátu D způsobenou odchylkou delta = y - m ⇒ k = D/delta

• Běh regresních testů na nové verzi programu.
• častější testování.
• Provedení testu, který by jinak bylo obtížné provést.
• Lepší využití prostředků.
• Konzistence opakovatelnosti testů.
• Vícenásobné použití testů.
• Zkrácení doby uvedení na trh.

• Nereálná očekávání.
• Slabá testovací praxe.
• Očekávání, že automatizovaný test nalezne mnoho nových defektů (typicky 85% manuální testování či návrh skriptu).
• Údržba automatizovaných testů.

• všechny možné kombinace

• selhání jsou způsobena interakcí pouze několika parametrů,
• testování kombinacemi pokrývající všechny možné k-tice,
• k-tice komprimovány do plných kombinací.

• 5 parametrů,
• 17 hodnot pro každý parametr

• 1.419.857 = 17⁵ kombinací
• 230 dnů testování

• Nezávislé parametry: 17 kombinací
• Párová závislost parametrů: 10 = 4 + 3 + 2 + 1 parametrových párů,
• 289 = 17² kombinací hodnot pro každý pár,
• 2890 = 289*10 párů parametrových hodnot,
• 289 kombinací obsahující všechny páry,
• 30 minut

Ortogonální pole je matice velikosti m x n, ve které při testování parametrických párů jednotlivé sloupce odpovídají faktorům (parametrům funkce, případně jiným hodnotám, na kterých závisí testovací případ) a řádky jednotlivým testovacím případům.

Ortogonální pole jsou označována podle toho, kolik úrovní (významných hodnot) umožňují jednotlivým faktorům. Ortogonální pole 2^{1},\; 3^{7} má celkem 8 faktorů. Jeden faktor může mít dvě významné hodnoty, a sedm dalších může mít až 3 významné hodnoty.

Pro použití této techniky je zapotřebí příklad nejprve zakódovat. Tato procedura je velmi snadná – nejprve nalezneme všechny faktory (parametry příkladu) a zjistíme, kolik mají úrovní. Poté nalezneme vhodné ortogonální pole.

Vybrané pole musí umožňovat alespoň tolik faktorů, kolik má náš případ. Dále je nutné, aby jednotlivé faktory měly dostatečný počet úrovní.

Nyní můžeme přejít k samotnému kódování. Každému parametru naší úlohy přiřadíme jeden sloupec – případné přebytečné sloupce můžeme ignorovat. Každé významné hodnotě přiřadíme jednu úroveň – pokud má sloupec více úrovní než potřebujeme, tak můžeme některé významné hodnotě přiřadit více úrovní, tím tuto hodnotu otestujeme více než ostatní (ale stále platí, že otestujeme každou parametrickou dvojici alespoň jednou).

V tomto okamžiku již můžeme pomocí našeho zakódování číst jednotlivé řádky ortogonálního pole – samotné testovací případy.

1. Ze zadání se identifikují faktory a úrovně
2. určím počet párově-ortogonálních čtverců jako N = max(faktorů-2, nejvyšší_úroveň)
3. najdu si čtverce v literatuře, (N+1) rozměrné
4. nyní generuji testovací případy: první faktor je číslo řádku, druhý faktor číslo sloupce, další hodnoty podle čísel na souřadnicích v jednotlivých čtvercích
5. vygeneruje mi to (N+1)^2 testovacích případů

Latinsky ctverec je matice n x n takova, ze kazdy element obsahuje cislo od 1 do n tak, ze se v zadnem sloupci nebo radku nevyskytuje vice nez jednou.

Parove ortogonalni latinske ctverce - kazdy element v danem ctverci vystupuje v relaci s kazdym elementem druheho ctverce prave jedenkrat - pro jakoukoliv mocninu prvocisla N existuje N - 1 parove ortogonalnich latinskych ctvercu velikosti N x N

Softwarová chyba je prezentace toho, že program nedělá něco, co jeho koncový uživatel předpokládá.

Term used to describe an error, flaw, mistake, failure, or fault in a computer program or system that produces an incorrect or unexpected result, or causes it to behave in unintended ways.

• Pochybení (Mistake): Akce člověka, která produkuje nesprávný výsledek.
• Vada (fault): Nesprávný krok, proces nebo definice dat v počítačovém programu. Výsledek pochybení. Potenciálně vede k selhání.
• Selhání (failure): Nesprávný výsledek. Projev vady.
• Chyba (error): Kvantitativní vyjádření toho, na kolik je výsledek nesprávný.

• Testování jednotek - funkční a strukturní požadavky na úrovni jednotky,
• Testování komponent - požadavky na úrovni komponenty (několik jednotek),
• Integrační testování - za předpokladu funkčních komponent testování kombinace komponent,
• Testování systému - zabývá se problematikou chování, ke kterému dochází v plně integrovaném systému.

• Formální testování je proces provádění testovacích aktivit a hlášení výsledků testů podle odsouhlaseného testovacího plánu.
• Akceptační testování je formální testování prováděného za účelem stanovit, zda systém splňuje akceptační kritéria a umožňuje zákazníkovi určit zda přijme systém či nikoliv.
• Systémové testování je proces testování integrovaného systému za účelem ověření, zda vyhovuje specifikovaným požadavkům.
• Regresní testování je částečné testování s cílem ověřit, že provedené modifikace nezpůsobují nechtěné vedlejší efekty nebo že modifikovaný systém stále splňuje požadavky.
• Hodnocení výkonnosti - určení dosažení efektivnosti operativní charakteristiky.

• Požadavek - podmínka nebo schopnost, kterou uživatel potřebuje k řešení problému nebo vyřešení úlohy.
• Specifikace - vyjádření množiny požadavků, kterým by měl produkt vyhovět.
• Testovací plán - dokument popisující zvolený přístup k zamýšleným testovacím aktivitám.
• Testovací případ - specifická množina testovacích dat společně s očekávanými výsledky vztažené k vybranému cílu testu.
• Návrh testu - výběr a specifikace množiny testovacích případů, které splnují úlohu testu nebo kritéria pokrytí.
• Dobrý test - nezanedbatelná pravděpodobnost detekce dosud neobjevené chyby.
• Úspěšný test - detekuje dosud neobjevenou chybu.

• Testovací data - vstupní data a podmínky pro soubory asociované s daným testovacím případem.
• Očekávané výsledky - predikované výstupní data a podmínky souborů asociované s daným testovacím případem.
• Orákulus je jakýkoliv program, proces nebo objem dat, které specifikují očekávaný výsledek množiny testů, pokud jsou aplikovány na testovaný objekt.
• Testovací procedura - dokument definující kroky směřující k pokrytí alespon části testovacího plánu nebo běhu množiny testovacích případů.
• Záznam testu - chronologický záznam všech význačných podrobností testovací aktivity.
• Platnost testu - stupen, jak dalece test dosahuje specifického cíl

Funkčnost Program má problém s funkčností, jestliže:

• nedělá něco, co by měl dělat nebo
• to dělá nevhodně, zmatečným způsobem či neúplně,
• lze některé operace provést obtížně,

• Konečná definice, co se „předpokládá“ od programu, žije pouze v mysli uživatele.
• Všechny programy mají problémy s funkčností vzhledem k různým uživatelům.
• Funkční problém je chybou, pokud očekávání uživatele jsou rozumná.

Chyby uživatelského rozhranní - vstupy Komunikace

• Jak lze nalézt, jak používat daný program?
• Jaká je nápověda, pokud uživatel udělá chybu či spustí < Help >?

Struktura příkazů

• Jak snadné je ztratit se v programu?
• Jaké chyby uživatel dělá, kolik je to stojí času a proč?

Chybějící příkazy

• Co chybí?
• Nutí program uživatele přemýšlet nějakým pevným, nepřirozeným nebo neefektivním způsobem?

Chyby uživatelského rozhranní - výstupy
Výkonnost

• Rychlost je základem interaktivního softwaru.
• Cokoliv vyvolává v uživateli pocit, že program pracuje pomalu, je problém.

Výstup

• Získá užitel, co potřebuje?
• Mají výstupní reporty smysl?
• Může uživatel přizpůsobit výstup svým potřebám?
• Lze přesměrovat výstup podle výběru uživatele na monitor, tiskárnu, či do souboru daného formátu?

• hranicni podminky ( numericke, mezni naroky na pamet )
• vypocetni chyby ( aritm. vypocty, zaokrouhlovani, chybne algoritmy )
• chyby zpracovani vyjimek

sekvencni

• pocatecni a jine specialni stavy ( po resetu programu se vse vrati do vychoziho bodu? )
• chyby rizeni ( nastane, pokud program provede chybny pristi krok )

paralelni

• chyby soubehu ( multiprocesorove systemy, obtizne se chyby opakuji )
• zatezove podminky ( program se chova chybne pokud se pretizi )

• hardware ( neexistujici zarizeni )
• rizeni zdroju a verzi (zakomponovani stare verze komponenty)
• dokumentace
• chyby testovani (chyby udelane testery)

• prikazy GOTO
• chyby zpracovani (vyhodnoceni aritm, algebr, matem. funkci, vyberu algoritmu)
• chyby logiky (spatne logicke operatory, neporozumeni semantice log. vyrazu)
• inicializacni chyby (opominuti incializace pracovniho prostoru, …)
• anomalie v toku dat nastane, kdyz treba existuje cesta, pri ktere se udela s daty neco neocekavaneho (pouziti neinicializovane promenne)

• neuplne, nejednoznacne pozadavky/specifikace
• chybne vlastnosti (chybejici nebo nevyzadane)
• interakce vlastnosti
• ⇒ prevence spociva v komunikaci clovek-clovek

• lze je nalezt ve specifikacich datovych objektu, jejich formatu, poctu objektu a jejich pocatecnich hodnotach
• dynamicke x staticke (ty dynamicke se hledaji hodne spatne)
• obsah, struktura, atributy (zakladem je explicitni dokumentace obsahu, struktury a atributu)

• to jsou chyby, ktere nam vychyta prekladac kodu (neukonceny komentar, strednik, …)

• tezko se lokalizuji
• jsou nepredikovatelne, casto se projevuji vzdalene od jejich priciny
• chyby hranic poli, nedefinovany ukazatel, cteni z neinicializovane pameti, memory leaks, …

• objekty, o ktere se zajimame (uzly)
• relace mezi uzly
• ktere objekty maji vztah s jinymi (hrany)
• vlastnosti asociovane s hranami (atributy hran)

• definuj graf, definuj relace
• navrhni testy pro pokryti uzlu
• navrhni testy pro pokryti hran
• otestuj vsechny atributy
• navrhni testy smycek```

• Pokrytí řádek - požaduje provedení každé řádky kódu alespoň jednou
• Pokrytí větví - znamená, že podmínka každého větvení musí být alespoň jednou pravdivá a jednou nepravdivá
• Pokrytí podmínek - zkontroluje všechny možné způsoby, za kterých daná podmínka je pravdivá či nepravdivá
• Úplné pokrytí cest - vyžaduje provedení všech možných různých úplných cest (v praxi neproveditelne)

• Metoda hlavních cest
• Metoda d-u cest
• Stavové automaty

Jednoduchá cesta . . .

• cesta z n_i do n_j, na které se žádný uzel neobjevuje více jak jedenkrát s vyjímkou, že počáteční a koncový uzel mohou být identické.

Hlavní cesta

• cesta z n_i do n_j je hlavní, jestliže je to jednoduchá cesta a není žádnou vlastní podcestou jakékoliv jiné jednoduché cesty(tj. je maximální)

Princip algoritmu

1. Nalezni cesty délky 0 (uzly).
2. Kombinuj cesty délky 0 do cest délky 1 (hrany).
3. Kombinuj cesty délky 1 do cest délky 2.
4. atd.

Označení
! . . . cesta nemůže být prodloužena
* . . . cesta tvoří smyčku

Tok datových hodnot: testy zajišťující, že hodnoty vzniklé na jednom místě jsou použity správně na jiných místech.
Definice def: místo, kde je hodnota proměnné uložena do paměti.
Užití use: místo, kde se přistupuje k hodnotě proměnné.
DU páry def - use: asociace určující přenosy hodnot.
Formalizace
V . . . množina proměnných asociovaná se softwarovým artefaktem.
def (n) (def (e)) . . . podmnožina množiny proměnných V , které jsou definovány uzlem n (hranou e).
use(n) (use(e)) . . . podmnožina množiny proměnných V , které jsou použity v uzlu n (na hraně e).

• Je systém v počátečním stavu?
  • Test nelze zahájit, pokud systém není potvrzeným způsobem v počátečním stavu.
  • Aplikace si uchovávají perzistentně svá nastavení.
  • Jestliže předchozí test selže, v jakém stavu se aplikace nachází?
• Má implementace skryté stavy?
  • Při testování software můžeme předpokládat věci, které nemusí obecně platit (např. že víme, ve kterém stavu se systém nachází).
  • Typicky se nejedná o jeden či dva skryté stavy, ale stavový prostor se zdvojnásobuje či jinak násobí.

1. identifikuj vstupy
2. definuj kody vstupu
3. idenfikuj stavy
4. definuj kodovani stavu
5. identifikuj vystupni akce
6. definuj kodovani vystupnich akci
7. specifikuj tabulku prechodu a tabulku vystupu - a zkontroluj ji
8. navrhni testy
9. proved testy
10. pro kazdy vstup over jak prechod tak i vystup

• kazdy test zacina v pocatecnim stavu
• z pocatecniho stavu se system privede nejkratsi cestou k vybranemu stavu, provede se zadany prechod a system se nejkratsi moznou cestou privede opet do pocatecniho stavu
• kazdy test stavi na predchozich jednodussich testech

Overime:

1. kodovani vstupu
2. kodovani vystupu
3. stavy
4. kazdy prechod

• použití temporální logiky (vyjádření času),
• systémy modelovány jako přechodové systémy s konečným počtem stavů.
• reaktivní, distribuované a paralelní systémy
• ověřuje se dosažitelnost, bezpečnost, živost…

• specikace i model vyjádřen jako automaty,
• oba automaty se porovnávají (jazyková inkluze, zjemnující uspořádání, pozorovací ekvivalence.)

Výhody

• úplná automatizace,
• vysoká rychlost,
• možnost verifikace i částečných specifikací,
• produkuje protipříklady.

Nevýhody

• problém exploze stavů,
• binární rozhodovací diagramy (BDD),
• nástroje jsou schopny zvládnout systémy s 100 - 200 stavovými proměnnými
• je možné zvládnout systémy s 10-120 stavy.

Kripkeho struktura je typ nedeterministického konečného automatu. Je to graf, který má dosažitelné stavy systému jako vrcholy a přechody mezi nimi jako hrany. Jde v podstatě o popis chování modelovaného systému, který je nezávislý na modelovacím jazyku.
Kripkeho struktura Je dána množinou atomických propozic AP.

Kripkeho struktura
Jde o trojici M = (S, T, I),

• S je konečná množina stavů
• T je přechodová relace
• I je interpretace AP

Rozšířená Kripkeho struktura
Jde o čtveřici M = (S, s0, T, I),

• s0 je počáteční stav

nebo pětici (S, s0, T, I, L),

• L je značkovací funkce (mapuje přechody T do množiny akcí proveditelných programem)

Vlastnosti modelů

• sada nedeterministických procesů s konečnou řídicí strukturou a reálnými hodinami,
• komunikují pomocí kanálů nebo sdílených proměnných

Systémový editor - Modelování

• jazyk nedeterministických podmíněných příkazů
• jednoduché datové typy (ohraničená celá čísla, pole, atd.)
• sítě automatů s hodinami a datovými proměnnými.

Verifikátor

• prověření všech možností dynamického chování modelu,
• kontrola invariantů a živosti prohledáváním stavového prostoru,
• dosažitelnost symbolických stavů reprezentovaných omezeními.

Simulátor

• grafická vizualizace a záznam možného chování systému (vyšetřování možných dynamických běhů systému)
• detekce vad modelu před jeho verikací,
• možnost vizualizace trasy generované verifikátorem (umožňuje analýzu záznamu běhů vedoucích k nežádaným stavům),

Časový automat je šestice (L; `0; C; A; E ; I), kde
L je množina pozic,
l0 je počáteční pozice,
C je množina hodin.
A je množina akcí, ko-akcí a interní fi-akce,
E je množina hran mezi pozicemi s akcí, stráží a množinou hodin, které se resetují,
I : L ! B(C) přiřazuje invarianty k pozicím.

Příklady y := 0 . . . resetování hodin y, press? a press! . . . označují akci a ko-akci (zde kanálovou synchronizaci).

Hodiny Ohodnocení hodin je přiřazení z množiny hodin do nezáporných reálných čísel. Z daného stavu je možné provést přechod pomocí akce nebo zpoždění

Sémantika časového automatu
Přednáška 7, slides 35-37

Výsledkem je kanál, synchronizuje se přes návěstí Expression! a Expression?

• Binární synchronizace - chan c, synchronizace hrany c! a c?

• Broadcast synchronizace - broadcast chan c, jedna hrana c! se všemi možnými c?, neblokuje.

• Urgentní synchronizace - urgent chan c, zpozdění není dovoleno, pokud je možný přechod na urgentním kanálu

Stavy automatu

• Initial pozice (initial) - Nová instance modelu se nachází v tomto stavu.

• Urgentní pozice (urgent) - Čas systému nemůže plynout, pokud se systém nachazí v urgentní pozici.

• Prováděcí pozice (commit) - Provadec stav se nemuze zpozdovat - Nasledující přechod musí zahrnovat jednu vystupí hranu vedoucí z prováděcí pozice. (Musí se pokračovat ven z commit pozice a nelze dělat nic jiného.)

Stráž je výraz, který lze vyhodnotit true/false. Stráže jsou přiřazeny k přechodům (hranám).

Invariant je podmínka, která musí být splněna kdykoli se automat nachází v daném stavu.

Dosažitelnost

• je nejjednodušší vlastností, tedy že existuje taková cesta, na které podmínka bude alespoň jednou splněna.
• E[] p: there exists a path where p always holds.

Bezpečnost

• Vlastnost, která nesmí nikdy nastat.
• Např. nelze překročit maximální teplotu nebo konec souboru a podobně. Často boundary check.
• Je formulována pozitivně - A[] p = E<>neg(p).

Živost

• Automat se jednou (eventually) dostane do určitého stavu.
• A<> p: for all paths p will eventually hold.

Recap

• E<> p: there exists a path where p eventually holds.
• A[] p: for all paths p always holds.
• E[] p: there exists a path where p always holds.
• A<> p: for all paths p will eventually hold.
• p –> q: whenever p holds q will eventually hold.

Invariant je podmínka, která musí být splněna kdykoli se automat nachází v daném stavu. Narozdíl od stráže neslouží jako kontrola podmínky, ale jde o součást stavu (automat se do daného stavu vůbec nemůže dostat, pokud není splněn invariant).

Stráž je výraz, kterou lze vyhodnotit true/false. Stráže jsou přiřazeny k přechodům (hranám).

• side-effect free (nelze přepisovat proměnné apod.)
• clocks, clock differences, integer variables and constants

• Abstrakce času
  • Logický čas - pracuje s částečným uspořádáním stavů/událostí v chování systému
  • Fyzický čas - měření doby uběhlé mezi dvěma stavy/událostmi
• Čas ve verifikaci modelů
  • Lineární čas - dovoluje se vyjadřovat pouze o dané lineární trase
  • Větvící se čas - dovoluje kvantifikovat možné budoucnosti počínaje daným stavem

skládá se z:

• atomických výroků
• logických spojek - negace, AND, OR, ⇒, ⇔
• kvantifikátorů
  • E - existuje
  • A - pro všechny
• temporálních operátorů
  • X (next) - platí v následujícím stavu cesty, znak kolečko
  • F (future) - platí v nějakém stavu cesty, znak kosočtverec
  • G (globally) - platí ve všech stavech cesty, znak čtverec
  • a U b (until) - a platí dokud neplatí b
  • a R b (release) - jakmile začne platit a, tak v dalším stavu přestává platit b a dál už neplatí. Tzn b platí naposled 1x dohromady spolu s a.

Z této abecedy se dají skládat:

• stavové formule - platí pro stav - skládají výroky pomocí logických spojek a kvantifikátorů
• běhové formule - platí pro cestu - rozšiřují stavové formule o temporální operátory

CTL logika je podmnožinou CTL*

V CTL* se temporální operátory mohou libovolně spojovat. V CTL musí být vždy v párech kvantifikátor-temporální operátor.

Minimální množina operátorů je: {false, OR, negace, EG, EU, EX}. Ostatní operátory jdou z těchto odvodit.

LTL je podmnožinou CTL*

Obsahuje pouze kvantifikátor A (takže se nepíše)

Ignoruje větvení.

Pro vyjádření logiky se používá BNF. Žádný výraz nesmí mít postranní efekty. Stavové formule obsahují stráže a mohou mít speciální hodnotu deadlock. Běhové formule:

• E<>a: existuje cesta, kde a bude splněno
• E[]a: existuje cesta, kde a je vždy splněno
• A<>a: pro všechny cesty bude a alespoň jednou splněno
• A[]a: pro všechny cesty bude a vždy splněno
• a –> b: pokud je a splněno, bude b nakonec splněno

• je jedna ze standartizovanych notaci
  • Z je prave jenom notace
  • neni exekucni
  • neni to programovaci jazyk
• Z notace je zalozena na:
  • teorii mnozin
  • matematicke logice (predikatovy kalkulus prveho radu)
  • na modelech
• System je modelovan pomoci:
  • stavu (na zaklade stavovych promennych a jejich hodnot)
  • operaci, ktere mohou menit stav

Schema = vzory deklaraci a omezeni

PVS specifikace obsahuje nekolik souboru, kazdy s jednou ci vice teoriemi - teorie muze importovat jine teorie.

• specifikacni jazyk
• ma podpurne nastroje
• daji se jim dokazovat vety
• implementovan v Common Lisp
• predikatova logika vyssiho radu

• dokazovac je interaktivni a vysoce zmechanizovany
• snaha dokazat vlastnosti specifikaci je nejefektivnejsi cesta k porozumeni jejich obsahu a k nalezeni chyb

1. vytvoreni specifikace
2. syntakticka analyza
3. typova kontrola
4. dokazovani

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 ne 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

slidy(pdf strany) 30-37

https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/11.javapathfinder.pdf

slidy(pdf strany) 19-28

https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/11.javapathfinder.pdf

Souvisi to s dedenim a polymorfismem.

1. SDA - state definition anomaly - přepisící metoda má jinou def množinu než přepisovaná
2. ITU - inconsistent type use - nepřepisování ale volání parent metod
3. SDIH - podobné SDA ale potomek přepíše něco v prarodiči a rodič pak používá špatně definovanou proměnnou
4. ACB1 - přepis konstruktoru, potomek pak používá něco co není definováno
5. SVA - přepsání metody v prarodiči, později rodič taky přepíše tu metodu a potomek začne volat rodiče, ne prarodiče

Typy testování: intra/inter metod a intra/inter tříd

Používá se k reprezentace interakce stavových prostorů, identifikace bodů integrace a testovacích požadavků.

V softwarových artefaktech se hledají vazby last-def a firt-use po volání metody a uvnitř metody.

Metriky produktu - popisuji charakteristiky jako je velikost, komplexity, navrhove vlastnosti, vykonnost, uroven kvality

Procesni metriky - mohou byt vyuzity pri zlepsovani vyvoje softwaru a procesu udrzby

• efektivita odstranovani defektu behem vyvoje
• vzor prirustku defektu behem testovani
• doba odezvy procesu oprav

Metriky projektu - popisuji charakteristiky projektu jeho provedeni

• pocet vyvojaru softwaru
• vyvoj personalu behem zivotniho cyklu softwaru
• cena, rozvrh, produktivita

Metriky kvality - podmnožiny SW metrik

• z pohledu zákazníka: např. MTTF - mean time to failure, intenzita defektů, hlášené problémy zákazníkem, spokojenost zákazníka
• průběhu procesu: zaznamenávání přírustků defektů, hustota defektů na KLOC, efektivnost odstraňování
• údržby: počet nevyřízených problémů, BMI - backlog management index - přibývají nové problémy rychleji než je odstraňujeme?

- pouziva atributy projektu nebo programovych modulu k odhadu poctu defektu v softwaru - parametry modelu jsou odhadovany na zaklade rady predchozich projektu

Weillova distribuce (jedna ze 3 znamych distribuci extremnich hodnot)

- rychlost defektu pozorovanych behem vyvojoveho procesu je positivne korelovana s rychlosti defektu v poli nasazeni - cim vice defektu je objeveno a odstraneno drive, tim mene jich zustane na pozdejsi faze

- pouziva prubezneho vyvoje vzoru defektu k odhadu spolehlivosti finalniho produktu - parametry dynamickych modelu jsou odhadovany na zaklade mnoha udaju zaznamenanych o hodnocenem produktu k danemu datu

- modely rustu spolehlivosti se obvykle odvozuji z dat faze formalniho testovani

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.

Explicitní vztah: Y = F(X)

• X .. vstup
• Y .. výstup

Jak se počítá kovarianční matice pro parametr p:

1. vyjádří se p
2. J je matice 1×2: derivace p podle x a derivace p podle y
3. kovarianční matice se počítá: J x matice 2×2 viz úkol x transponovaná J

Implicitní vztah: skalární funkce F(X,Y)

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

slidy(pdf strany) 19-21

https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/13.statisticketestovani.pdf