Model checking of control-user systems
Řada reálných softwarových systémů (tzv. kontroler-uživatel systémů) je složena ze stabilní části (kontroler) a libovolného počtu dynamických komponent stejného typu (uživatel). Modely těchto systémů jsou parametrizovány počtem komponent uživatelů a tudíž stavové prostory těchto modelů mají potenciá...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2009.
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/4042/fi_d/ |
| Shrnutí: | Řada reálných softwarových systémů (tzv. kontroler-uživatel systémů) je složena ze stabilní části (kontroler) a libovolného počtu dynamických komponent stejného typu (uživatel). Modely těchto systémů jsou parametrizovány počtem komponent uživatelů a tudíž stavové prostory těchto modelů mají potenciálně nekonečně mnoho stavů. Tradiční techniky na ověřování modelu (model checking) proto mohou být použity pouze na verifikaci konkrétních instancí těchto systémů, ale ne na systém jako celek. Tato práce prezentuje tři plně automatické techniky na verifikaci vlastností systémů typu kontroler-uživatel. První technika umožňuje verifikovat vlastnosti dosažitelnosti. Popisovaný algoritmus je úplný, je typu on-the-fly a umožňuje také souběžnou verifikaci více vlastností. Druhý algoritmus, využívající první přístup, odpovídá na otázky typu "Kolik nejvíce uživatelů může být v dané specifické situaci?". Třetí algoritmus ověřuje s využitím dvou dříve popsaných technik vlastnosti logiky SE-LTL na syst. Many real software systems, so called control-user systems, are composed of a stable part (control component) and a number of dynamic components of the same type (user components). Models of these systems are parametrised by the number of user components and thus have infinite size of state space. Traditional model checking techniques can be used to verify only specific instances of the systems. This work presents three fully automatic techniques for verification of properties of control-user systems. The first serves for verification of reachability properties. This complete technique can be used on-the-fly and enables verification of several reachability properties simultaneously. The second algorithm, using the first technique, answers questions like \emph{"What is the maximal possible number of users which could be in a specific situation?"}. The third described algorithm verifies, employing the two previous techniques, state-event LTL properties of control-user models. Appl. |
|---|---|
| Popis jednotky: | Vedoucí práce: Ivana Černá. |
| Fyzický popis: | v, 117 s. |