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/ |
| LEADER | 05644ctm a22009017a 4500 | ||
|---|---|---|---|
| 001 | MUB01000584555 | ||
| 003 | CZ BrMU | ||
| 005 | 20240510120527.0 | ||
| 008 | 090526s2009 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2018-08-31 | ||
| 035 | |a (ISMU-VSKP)96943 | ||
| 040 | |a BOD114 |b cze |d BOD018 | ||
| 072 | 7 | |a 004.4/.6 |x Programování. Software |2 Konspekt |9 23 | |
| 080 | |a 004.455 |2 MRF | ||
| 080 | |a 303.732.4 |2 MRF | ||
| 080 | |a (043.3) |2 MRF | ||
| 080 | |a 004.03 |2 MRF | ||
| 100 | 1 | |a Moravcová Vařeková, Pavlína |% UČO 4042 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Model checking of control-user systems. |y eng |
| 245 | 1 | 0 | |a Model checking of control-user systems |h [rukopis] / |c Pavlína Moravcová Vařeková. |
| 260 | |c 2009. | ||
| 300 | |a v, 117 s. | ||
| 500 | |a Vedoucí práce: Ivana Černá. | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2009. | ||
| 520 | 2 | |a Ř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. |% cze | |
| 520 | 2 | 9 | |a 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. |9 eng |
| 650 | 0 | 7 | |a klient/server software |7 ph121616 |2 czenas |
| 650 | 0 | 7 | |a systémová analýza |7 ph116372 |2 czenas |
| 650 | 0 | 7 | |a počítačové systémy |7 ph115866 |2 czenas |
| 650 | 0 | 9 | |a computer systems |2 eczenas |
| 650 | 0 | 9 | |a client-server software |2 eczenas |
| 650 | 0 | 9 | |a system analysis |2 eczenas |
| 655 | 7 | |a disertace |7 fd132024 |2 czenas | |
| 655 | 9 | |a dissertations |2 eczenas | |
| 658 | |a Informatika (čtyřleté) |b Informatika |c FI D-IN4 IN (IN) |2 CZ-BrMU | ||
| 700 | 1 | |a Černá, Ivana, |d 1963- |7 mub2011658599 |% UČO 1419 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Fakulta informatiky |7 kn20010709274 |4 dgg | |
| 856 | 4 | 1 | |u http://is.muni.cz/th/4042/fi_d/ |
| CAT | |c 20090526 |l MUB01 |h 0451 | ||
| CAT | |c 20091203 |l MUB01 |h 0229 | ||
| CAT | |c 20091203 |l MUB01 |h 1912 | ||
| CAT | |a KOZOVA |b 02 |c 20100113 |l MUB01 |h 1028 | ||
| CAT | |a KOZOVA |b 02 |c 20100113 |l MUB01 |h 1034 | ||
| CAT | |a KOZOVA |b 02 |c 20100113 |l MUB01 |h 1109 | ||
| CAT | |c 20100428 |l MUB01 |h 1012 | ||
| CAT | |a BATCH-UPD |b 00 |c 20100501 |l MUB01 |h 1212 | ||
| CAT | |a BATCH-UPD |b 00 |c 20100929 |l MUB01 |h 0334 | ||
| CAT | |c 20110627 |l MUB01 |h 1915 | ||
| CAT | |c 20110627 |l MUB01 |h 2323 | ||
| CAT | |a KOZOVAX |b 02 |c 20110909 |l MUB01 |h 0939 | ||
| CAT | |a batch |b 00 |c 20120324 |l MUB01 |h 0125 | ||
| CAT | |a POSPEL |b 02 |c 20120417 |l MUB01 |h 0740 | ||
| CAT | |a POSPEL |b 02 |c 20120626 |l MUB01 |h 0801 | ||
| CAT | |a HANAV |b 02 |c 20120924 |l MUB01 |h 1504 | ||
| CAT | |a BATCH |b 00 |c 20130303 |l MUB01 |h 1102 | ||
| CAT | |a HANAV |b 02 |c 20130513 |l MUB01 |h 1149 | ||
| CAT | |a POSPEL |b 02 |c 20130530 |l MUB01 |h 0738 | ||
| CAT | |a POSPEL |b 02 |c 20130605 |l MUB01 |h 0736 | ||
| CAT | |a POSPEL |b 02 |c 20130821 |l MUB01 |h 1021 | ||
| CAT | |a POSPEL |b 02 |c 20140107 |l MUB01 |h 1224 | ||
| CAT | |c 20150901 |l MUB01 |h 1443 | ||
| CAT | |c 20150921 |l MUB01 |h 1404 | ||
| CAT | |a HANAV |b 02 |c 20151102 |l MUB01 |h 1302 | ||
| CAT | |a BATCH |b 00 |c 20151226 |l MUB01 |h 0017 | ||
| CAT | |c 20180831 |l MUB01 |h 1052 | ||
| CAT | |c 20210614 |l MUB01 |h 0938 | ||
| CAT | |c 20210614 |l MUB01 |h 1927 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1146 | ||
| CAT | |a HANAV |b 02 |c 20211116 |l MUB01 |h 0031 | ||
| CAT | |a VESELAX |b 02 |c 20240510 |l MUB01 |h 1028 | ||
| CAT | |a VESELAX |b 02 |c 20240510 |l MUB01 |h 1031 | ||
| CAT | |a VESELAX |b 02 |c 20240510 |l MUB01 |h 1031 | ||
| CAT | |a VESELAX |b 02 |c 20240510 |l MUB01 |h 1032 | ||
| CAT | |a VESELAX |b 02 |c 20240510 |l MUB01 |h 1205 | ||
| LOW | |a POSLANO DO SKCR |b 2018-08-31 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |2 SKLAD |b sklad |3 Diz. práce 2009 |5 42005D2583 |8 20100113 |f 72 |f Týdenní |r 20100113 |
| AVA | |a INF50 |b FI |c sklad |d Diz. práce 2009 |e available |t K dispozici |f 1 |g 0 |h N |i 0 |j SKLAD | ||