Analýza a návrh softwarových systémů: Porovnání verzí
Z ωικι.matfyz.cz
m (→Vyjadřovací prostředky a metody (datové modelování, procesní modelování - funkční a dynamické)) |
m (→Plánování a řízení projektů, alokace zdrojů, použití metrik, řízení kvality, stupně zralosti sw. týmů (CMM)) |
||
Řádka 199: | Řádka 199: | ||
== Návrh relačních schémat v 3NF == | == Návrh relačních schémat v 3NF == | ||
== Modely životního cyklu softwarových systémů == | == Modely životního cyklu softwarových systémů == | ||
− | == Plánování a řízení projektů | + | == Plánování a řízení projektů == |
+ | === Alokace zdrojů === | ||
+ | === Použití metrik === | ||
+ | === Řízení kvality === | ||
+ | === Stupně zralosti sw. týmů (CMM) === | ||
+ | |||
== CASE systémy == | == CASE systémy == | ||
== Třívrstvá struktura informačních systémů, klinet/server == | == Třívrstvá struktura informačních systémů, klinet/server == |
Verze z 11. 5. 2007, 19:52
Obsah
- 1 Zdroje
- 2 Zpracování jednotlivých otázek
- 2.1 Algebraické specifikace, formální popis datových struktur
- 2.2 Modelově orientované metody
- 2.3 Analýza algoritmů
- 2.4 Petriho sítě
- 2.5 Vyjadřovací prostředky a metody
- 2.6 Strukturované analýzy návrhu informačních systémů
- 2.7 Konceptuální modelování, databázové modelování, implementace
- 2.8 E-R schémata a jejich transformace do relačního modelu
- 2.9 Návrh relačních schémat v 3NF
- 2.10 Modely životního cyklu softwarových systémů
- 2.11 Plánování a řízení projektů
- 2.12 CASE systémy
- 2.13 Třívrstvá struktura informačních systémů, klinet/server
- 2.14 XML a značkovací jazyky
- 2.15 Objektová analýza a návrh (UML)
- 2.16 Informační bezpečnost
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):
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)