Verze z 11. 5. 2007, 20:52

Zdroje

• Materiály přednášky Software design and implementation na univerzitě v Severní Carolině

Zpracování jednotlivých otázek

Algebraické specifikace, formální popis datových struktur

Příklad - množina INTů:

sorts: SET, INT, BOOLEAN          | vsechny vyuzivane typy
operations:                       | popisuji syntaxi daneho ADT
  - empty:            --> SET     | generator
  - insert: SET x INT --> SET     | generator
  x delete: SET x INT --> SET
  x member: SET x INT --> BOOLEAN
axioms:                           | popisuji semantiku specifikovanych operaci
  member(empty(),j) = false       | axiomy pro vsechny co nejsou generator se vsema moznyma ..
  member(insert(S,j),k) =         | generatorama na vstupu
    if (j=k) then true else member(S,k)
  delete(empty(),j) = empty()
  delete(insert(S,j),k) =
    if (j=k) then delete(S,j) 
             else insert(delete(S,k),j)

Modelově orientované metody

Z

VDM

Analýza algoritmů

• validace = "Are we building the right product?"
  • nebo jinými slovy - jde o kontrolu, zda-li daný produkt odpovídá reálným požadavkům
• verifikace = "Are we building the product right?"
  • neboli - jde o kontrolu, zda-li daný produkt odpovídá výchozí specifikaci

Hoaerova logika

• viz wen: Hoare logic
• cílem je, aby se dala formálně dokazovat korektnost programů pomocí rigorózních prostředků matematické logiky
• základem je Hoare triple, popisující jak kousek kódu změnil stav výpočtu - $ \{P\} C \{Q\}\! $
  • kde P a Q jsou assertions a C je příkaz. P nazýváme precondition, Q postcondition. Obojí jsou formule predikátové logiky.
• Hoaerova logika (dále jen HL) obsahuje axiomy a odvozovací pravidla pro všechny konstrukty jednoduchého imperativního programovacího jazyka
• Standardní HL poskytuje pouze partial correctness, neboli říká, že pokud před provedením C platí P, pak po jeho provedení platí Q, nebo C neskončí. Existuje ale rozšíření poskytující total correctness.

Pravidla jsou:

• Empty statement axiom schema:

$ \frac{}{\{P\}\ \textbf{pass}\ \{P\}} \! $

• Assignment axiom schema:

$ \frac{}{\{P[x/E]\}\ x:=E \ \{P\} } \! $

• Rule of composition:

$ \frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \! $

• Conditional rule:

$ \frac { \{B \wedge P\}\ S\ \{Q\}\ ,\ \{\neg B \wedge P \}\ T\ \{Q\} } { \{P\}\ \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif}\ \{Q\} } \! $

• While rule:

$ \frac { \{P \wedge B \}\ S\ \{P\} } { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} }\! $

• Consequence rule:

$ \frac { P^\prime \rightarrow\ P\ ,\ \lbrace P \rbrace\ S\ \lbrace Q \rbrace\ ,\ Q \rightarrow\ Q^\prime } { \lbrace P^\prime\ \rbrace\ S\ \lbrace Q^\prime\rbrace }\! $

• While rule for total correctness:

$ \frac { \{P \wedge B \wedge t = z \}\ S\ \{P \wedge t < z \} \ ,\ P \rightarrow t \geq 0} { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} } \! $

Jak se to celé používá je hezky vysvětleno tady, nebudu se to snažit zreplikovat.

Dynamická logika

• viz wen: Dynamic logic (modal logic)
• Navrhl Vaughan Pratt v roce 1974
• Je rozšířením modální logiky zaměřené na dedukci o počítačových programech (ovšem později se začla využívat i jinde)
• Modální logika je charakteristická svými dvěma modálními operátory:
  • $ \Box p $ - říká že p platí vždy
  • $ \Diamond p $ - říká že p může platit
    • platí pro ně $ \Box p \leftrightarrow \lnot \Diamond \lnot p $ a $ \Diamond p \leftrightarrow \lnot \Box \lnot p $
• DL přidává ke dvou termům logik prvního řádu (tvrzení a data) ještě třetí typ termu - akci
• Dynamická logika (dále jen DL) toto rozšiřuje přidáním dvou modálních operátorů pro akce:
  • $ [ a ]\! $, kde $ [ a ] p\! $ znamená, že po provedení akce a musí p platit
  • $ \langle a \rangle $, kde $ \langle a \rangle p $ znamená, že po provedení akce a může p platit
    • opět samozřejmě platí $ \langle a \rangle p \leftrightarrow \lnot [ a ] \lnot p $ a $ [ a ] p \leftrightarrow \lnot \langle a \rangle \lnot p\! $
• DL umožňuje skládání akcí, pro jejich zápis se dá využít notace regulárních výrazů:
  • $ a | b\! $ .. provede se a nebo b
  • $ a ; b\! $ .. provede se nejprve a, pak b
  • $ a*\! $ .. a se provede 0 nebo vícekrát
• Dále jsou k dispozici konstantní akce:
  • $ 0\! $ .. nic neudělá a neskončí (aka BLOCK)
  • $ 1\! $ .. nic neudělá a skončí (aka NOP)
• Krom defaultních jsou definovány tyto axiomy:
  • A1. $ [ 0 ] p \! $
  • A2. $ [ 1 ] p \leftrightarrow p \! $
  • A3. $ [ a | b ] p \leftrightarrow [ a ] p \wedge [ b ] p \! $
  • A4. $ [ a ; b ] p \leftrightarrow [ a ] [ b ] p \! $
  • A5. $ [ a * ] p \leftrightarrow p \wedge [ a ] [ a * ] p\! $
  • A6. $ p \wedge [ a * ] ( p \rightarrow [ a ] p ) \rightarrow [ a * ] p \! $ (s akcí n:=n+1 odpovídá matematické indukci)
  • speciální axiomy
  • A7. axiom schema $ [ x := e ] \Phi (x) \leftrightarrow \Phi (e) $, odpovídá přiřazení z Hoareovy logiky. Tedy $ \Phi (e) $ odpovídá fli ve které jsou všechny výskyty x nahrazeny výrazem e.
  • A8. $ [ p ? ] q \leftrightarrow p \rightarrow q $, kde p? je speciální akce definována ke každému tvrzení taková, že p? odpovídá NOP pokud je p true, jinak je to BLOCK. If p then a else b se dá tedy zapsat jako $ (p?;a)|(\lnot p?;b)\! $
• $ x:=?\! $ znamená přiřazení libovolné hodnoty do x, a tedy $ [x:=?]\! $ odpovídá obecnému kvantifikátoru, zatímco $ \langle x:=? \rangle $ odpovídá existenčnímu

$ \{p\} a \{q\}\! $ z HL se dá v DL zapsat jako $ p \rightarrow [a]q\! $

Stejně jako HL se v ní nedajá elegantně vyjádřit konkurentní chování (zatímco sekvenční se zapisuje hezky). To ovšem jde v TL (temporální).

Temporální logika

• viz wen:Temporal logic
• přináší prvek času, pravdivost tvrzení se tedy může v závislosti na čase měnit
  • například "mám hlad" je pravdivé jenom někdy (třeba teď ;), díky temporální logice můžeme být proto přesnější a říct "budu mít hlad dokud se nenajím"
  • přínos pro formální verifikaci je zřejmý - snadno můžeme zapsat tvrzení typu "kdykoli příjde požadavek, zařízení může být zpřístupněno, ale v žádném případě nebude současně zpřístupněno dvěma žadatelům"
• je několik variací - linear temporal logic (AKA LTL, existuje jen jedna časová linie) a branching logic (více možných časových linií = nedeterminismus, zřejmě má stejnou sílu jako lineární)
• dva druhy operátorů
  • logical operators (klasika: $ \neg,\or,\and,\rightarrow $)
  • modal operators (operátory, které říkají například že fle musí někdy v budoucnu platit, nebo že musí platit odteď nafurt)

Modální operátory v LTL jsou následující (přeloženo z wikipedie):

Dalo by se zredukovat na dva z těchto operátorů, protože vždy platí:

• F $ \phi $ = true U $ \phi $
• G $ \phi $ = false R $ \phi $ = $ \neg $ F $ \neg $$ \phi $
• $ \psi $ R $ \phi $ = $ \neg $($ \neg $$ \psi $ U $ \neg $$ \phi $)

Petriho sítě

• viz wen: Petri net
• matematická reprezentace diskrétních distribuovaných systémů
• vynalezl je Carl Adam Petri ve své Ph.D práci v roce 1962
• orientované bipartitní grafy ze dvěma druhy uzlů - místa a přechody
• nedeterministické! (není přesně definováno ktery z možných přechodů se nastartuje)

Formálně: Petriho síť je pětice $ (P,T,F,M_0,W)\! $, kde:

• $ P\! $ je seznam míst
• $ T\! $ je seznam přechodů
• $ F\! $ je seznam hran (žádná hrana nesmí spojovat dvě místa nebo dva přechody, tedy $ F \subseteq (P \times T) \cup (T \times P) $)
• $ M_0 : S \to \mathbb{N} $ je iniciální označkování, v každém místě $ p \in P $, existuje $ n_p \in \mathbb{N} $ tokenů
• $ W : F \to \mathbb{N^+} $ je množiná váh hran, které každé hraně $ f \in F $ přiřazují $ n \in \mathbb{N^+} $ které označuje kolik tokenů je při přechodu danou hranou navazujícím přechodem zkonzumováno, případně kolik tokenů výchozí přechod generuje

• stav sítě je vektor, kde v každé položce je počet tokenů aktuálně obsažený v místě s příslušným indexem
• další vlastnosti
  • state-transition list
  • state-transition matrix
  • reachability
  • liveness
  • boundedness
• možná rozšíření
  • barevné petriho sítě (tokeny je možno rozlišovat)
  • prioritizované petriho sítě (přechody mají priority)

• hierarchie petriho sítí
  • state machine (každý přechod má 1 in a 1 out hranu => může vzniknout konflikt), marked graph (každé místo má 1 in a 1 out hranu => může vzniknout konkurence)
  • free choice (hrana je buď jediná která vystupuje z místa, nebo jediná která vstupuje do přechodu => může být konflikt i konkurence, ale ne najednou)
  • extended free choice (taková, která se dá transformovat na FC)
  • asymetric choice (konkurence i konflikt povoleny, ale ne asymetricky)
  • petri net (všecko povoleno)

Vyjadřovací prostředky a metody

Datové modelování

Procesní modelování (funkční a dynamické)

Strukturované analýzy návrhu informačních systémů

Konceptuální modelování, databázové modelování, implementace

E-R schémata a jejich transformace do relačního modelu

Návrh relačních schémat v 3NF

Modely životního cyklu softwarových systémů

Plánování a řízení projektů

Alokace zdrojů

Použití metrik

Řízení kvality

Stupně zralosti sw. týmů (CMM)

CASE systémy

Třívrstvá struktura informačních systémů, klinet/server

XML a značkovací jazyky

Objektová analýza a návrh (UML)

Informační bezpečnost