Analýza a návrh softwarových systémů

Z ωικι.matfyz.cz
Verze z 11. 5. 2007, 20:48, kterou vytvořil Srakyi (diskuse | příspěvky) (Modelově orientované metody: Z, VDM)

Přejít na: navigace, hledání

Zdroje

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ů: Hoareova metoda, dynamická logika, temporální logika

  • 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):

Textově Symbolicky Význam
Unární operátory:
N $ \phi $ $ \circ \phi $ Next: $ \phi $ musí platit v příštím stavu. (někdy se používá X)
G $ \phi $ $ \Box \phi $ Globally: $ \phi $ musí platit od teď pořád.
F $ \phi $ $ \Diamond \phi $ Finally: $ \phi $ musí platit někdy v budoucnu.
Binární operátory:
$ \psi $ U $ \phi $ $ \psi\mathcal{U}\phi $ Until: $ \phi $ platí v teď nebo v budoucnu a $ \psi $ musí platit až do té doby. Pak už $ \psi $ platit nemusí.
$ \psi $ R $ \phi $ $ \psi\mathcal{R}\phi $ Release: $ \psi $ uvolňuje $ \phi $ jestliže $ \phi $ platí do přvní pozice ve které $ \psi $ platí (nebo navždy, pokud taková pozice neexistuje).

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