CRHOVÁ, Jitka. Distributed Modular Model Checking (abstract). In The Seventeenth IEEE International Conference on Automated Software Engineering. Los Alamitos: IEEE Computer Society, 2002, s. 312. ISBN 0-7695-1736-6.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Distributed Modular Model Checking (abstract)
Autoři CRHOVÁ, Jitka (203 Česká republika, garant).
Vydání Los Alamitos, The Seventeenth IEEE International Conference on Automated Software Engineering, s. 312-312, 2002.
Nakladatel IEEE Computer Society
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 20206 Computer hardware and architecture
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/02:00006592
Organizační jednotka Fakulta informatiky
ISBN 0-7695-1736-6
Klíčová slova anglicky formal methods; distributed model checking; modular model checking
Štítky distributed model checking, Formal Methods, modular model checking
Změnil Změnila: Mgr. Jitka Žídková, učo 2922. Změněno: 14. 5. 2003 14:10.
Anotace
A distributed model checking algorithm is presented. It is designed to be run on a network of workstations that communicate via message passing. The algorithm handles large state spaces by partitioning them into smaller units. Such a partition of state space into partial state spaces can be employed to perform several smaller verification problems independently on several computers increasing thus not only speeding up the verification, but most importantly the available memory. We also suggest partition function that can be used as input to the ditributed algorithm. For software systems a quite successful approach is to partition them following the syntactical structure of the program. Other state based temporal logics and various model checking algorithms can be adapted easily as well.
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: 14. 5. 2024 21:59