Disjunctive Modal Transition Systems
Otázka korektnosti je bezpochyby zásadním faktorem při návrhu počítačových systémů, což dělá z oblasti specifikace a verifikace důležitou součást informatiky. K tomu, abychom mohli v této oblasti použít formálních metod, potřebujeme dobrý specifikační formalismum. Jednou možností je popsat požadovan...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2012
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/72525/fi_d/ |
| LEADER | 05152ctm a22007817a 4500 | ||
|---|---|---|---|
| 001 | MUB01000718360 | ||
| 003 | CZ BrMU | ||
| 005 | 20240513151714.0 | ||
| 008 | 120606s2012 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2020-04-29 | ||
| 035 | |a (ISMU-VSKP)139137 | ||
| 040 | |a BOD114 |b cze |d BOD018 | ||
| 072 | 7 | |a 004 |x Počítačová věda. Výpočetní technika. Informační technologie |2 Konspekt |9 23 | |
| 080 | |a 004.03 |2 MRF | ||
| 080 | |a 004.052.42 |2 MRF | ||
| 080 | |a 007+004 |2 MRF | ||
| 100 | 1 | |a Beneš, Nikola |% UČO 72525 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Disjunctive Modal Transition Systems |y eng |
| 245 | 1 | 0 | |a Disjunctive Modal Transition Systems |h [rukopis] / |c Nikola Beneš |
| 260 | |c 2012 | ||
| 300 | |a v, 95 s. | ||
| 500 | |a Vedoucí práce: Ivana Černá | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2012 | ||
| 520 | 2 | |a Otázka korektnosti je bezpochyby zásadním faktorem při návrhu počítačových systémů, což dělá z oblasti specifikace a verifikace důležitou součást informatiky. K tomu, abychom mohli v této oblasti použít formálních metod, potřebujeme dobrý specifikační formalismum. Jednou možností je popsat požadované vlastnosti systému pomocí formulí vhodné logiky. Jinou možností je přístup založený na chování, při němž se jak specifikace, tak implementace systému popisují za použití stejného formalismu a správnost systému se pak ověřuje za použití jistého druhu ekvivalence či jiné relace. V této práci se zaměřujeme hlavně na tento přístup, ačkoli i ten dáváme do souvislosti s přístupem logickým. Modální přechodové systémy jsou formalismem, který je schopen popisovat specifikace i implementace. Jeho hlavním přínosem je to, že umožnuje jistou volnost ve specifikacích, možnost nechat části systému nedospecifikovány. Toho je dosaženo rozšířením standardních přechodových systémů o dva druhy přechodů - tzv. |% cze | |
| 520 | 2 | 9 | |a The question of correctness is without doubt a crucial issue in the design of computer systems, making the field of specification and verification an important part of computer science. To employ formal methods in this field, we need to have a good specification formalism. One option is to specify the desired properties of a system as formulae of a suitable logic. Another option is the behavioural approach, describing both the specification and the implementation of the system in the same formalism, employing some kind of equivalence or refinement checking to establish the system’s correctness. We focus mainly on this approach in this thesis, although we also make some connection to the logical one. Modal transition systems is a formalism that is able to describe specifications as well as implementations. Its main feature is that it allows for looseness in specifications, leaving some parts of the system underspecified. It does so by extending the classical notion of a transition syste |9 eng |
| 650 | 0 | 7 | |a formální verifikace |7 ph755479 |2 czenas |
| 650 | 0 | 7 | |a počítačové systémy |7 ph115866 |2 czenas |
| 650 | 0 | 7 | |a informační systémy |7 ph114774 |2 czenas |
| 650 | 0 | 9 | |a computer systems |2 eczenas |
| 650 | 0 | 9 | |a Formal methods |2 eczenas |
| 650 | 0 | 9 | |a formal verification |2 eczenas |
| 650 | 0 | 9 | |a information systems |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/72525/fi_d/ |
| CAT | |c 20120606 |l MUB01 |h 0420 | ||
| 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 20130304 |l MUB01 |h 1424 | ||
| 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 | |a VESELA |b 02 |c 20140314 |l MUB01 |h 1051 | ||
| CAT | |c 20140911 |l MUB01 |h 1608 | ||
| CAT | |c 20140912 |l MUB01 |h 1102 | ||
| CAT | |c 20150703 |l MUB01 |h 1204 | ||
| CAT | |c 20150901 |l MUB01 |h 1448 | ||
| CAT | |c 20150921 |l MUB01 |h 1409 | ||
| CAT | |a VACOVAX |b 02 |c 20151012 |l MUB01 |h 1025 | ||
| CAT | |a HANAV |b 02 |c 20151102 |l MUB01 |h 1302 | ||
| CAT | |a BATCH |b 00 |c 20151226 |l MUB01 |h 0241 | ||
| CAT | |a HANAV |b 02 |c 20160329 |l MUB01 |h 1157 | ||
| CAT | |c 20200429 |l MUB01 |h 1338 | ||
| CAT | |c 20210614 |l MUB01 |h 0959 | ||
| CAT | |c 20210614 |l MUB01 |h 1947 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1214 | ||
| CAT | |a HANAV |b 02 |c 20211116 |l MUB01 |h 0031 | ||
| CAT | |a VESELAX |b 02 |c 20240513 |l MUB01 |h 1516 | ||
| CAT | |a VESELAX |b 02 |c 20240513 |l MUB01 |h 1517 | ||
| LOW | |a POSLANO DO SKCR |b 2020-04-29 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |3 Diz. práce 2012 |5 42005D2619 |8 20140313 |f 72 |f Týdenní |r 20140313 |
| AVA | |a INF50 |b FI |d Diz. práce 2012 |e available |t K dispozici |f 1 |g 0 |h N |i 0 | ||