BRIM, Luboš. Automatizovaná formální verifikace. In XXI. conference EurOpen 2002. Znojmo, Czech republic. Znojmo, Czech Republic: EuroOpen.cz, Praha. s. 1-7. ISBN 80-86583-00-7. 2002.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Automatizovaná formální verifikace
Název anglicky Automated formal verification
Autoři BRIM, Luboš (203 Česká republika, garant).
Vydání Znojmo, Czech Republic, XXI. conference EurOpen 2002. Znojmo, Czech republic, s. 1-7, 2002.
Nakladatel EuroOpen.cz, Praha
Další údaje
Originální jazyk čeština
Typ výsledku Stať ve sborníku
Obor 20206 Computer hardware and architecture
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/02:00006441
Organizační jednotka Fakulta informatiky
ISBN 80-86583-00-7
Klíčová slova anglicky verification
Štítky verification
Změnil Změnil: prof. RNDr. Luboš Brim, CSc., učo 197. Změněno: 10. 1. 2006 15:01.
Anotace
V posledních letech stále více narůstá význam formální verifikace komplexních hardwarových a softwarových systémů jako alternativního přístupu ke zvýšení správnosti, spolehlivosti a kvality. Automatizovaná formální verifikace částečně odstraňuje omezení tradičních metod jakými jsou simulace a testování. V příspěvku se zaměříme na přehled současného stavu, charakterizujeme postavení formálních metod verifikace v procesu vývoje komplexních systémů. Podrobněji pak pojednáme o tzv. ověřování správnosti modelu (Model Checking), který je v současné době již standardně používán v průmyslové praxi.
Anotace anglicky
In the paper we give an overview of the current state in the formal verification of hardware and software systems with particular emphasis on model checking and its possibilities and limitations.
Návaznosti
GA201/00/1023, projekt VaVNázev: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů
VytisknoutZobrazeno: 19. 4. 2024 08:26