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/ |
| Shrnutí: | 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. 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 |
|---|---|
| Popis jednotky: | Vedoucí práce: Ivana Černá |
| Fyzický popis: | v, 95 s. |