Parallel Model Checking and the FMICS-jETI Platform
BARNAT, Jiri, Lubos BRIM a Martin LEUCKER. Parallel Model Checking and the FMICS-jETI Platform. In Proceedings Twelfth IEEE International Conference on Engineering of Complex Computer Systems. Los Alamitos: IEEE Computer Society, 2007, s. 330-339. ISBN 0-7695-2895-3. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | Parallel Model Checking and the FMICS-jETI Platform |
Název česky | Paralelní ověřování modelů a platforma FMICS-jETI |
Autoři | BARNAT, Jiri (203 Česká republika), Lubos BRIM (203 Česká republika, garant) a Martin LEUCKER (276 Německo). |
Vydání | Los Alamitos, Proceedings Twelfth IEEE International Conference on Engineering of Complex Computer Systems, od s. 330-339, 10 s. 2007. |
Nakladatel | IEEE Computer Society |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Stať ve sborníku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Nový Zéland |
Utajení | není předmětem státního či obchodního tajemství |
Kód RIV | RIV/00216224:14330/07:00019460 |
Organizační jednotka | Fakulta informatiky |
ISBN | 0-7695-2895-3 |
UT WoS | 000248574000034 |
Klíčová slova anglicky | Parallel Model Checking; FMICS-jETI platform |
Štítky | FMICS-jETI platform, parallel model checking |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 1. 6. 2009 21:05. |
Anotace |
---|
In this paper we summarize parallel algorithms for enumerative model checking of properties formulated in linear time temporal logic (LTL) as well as a fragment of the mu-calculus which naturally subsumes the branching time logic CTL (computation tree logic). We also indicate how to provide parallel model checking applications as services for integrated modelling, analysis, and verification using thee FMICS-jETI platform. |
Anotace česky |
---|
V tomto článku jsou shrnuty algoritmy pro enumerativní ověřování modelu vlastností fomrulovaných v lineární temporální logice (LTL) a fragmentu mu-kalkulu, který přirozeně obsahuje také výpočtovou logiku větvícího se času (CTL). Také indikujeme použití aplikace jako služby pro integrované modelování, analýzu a verifikaci v rámci FMICS-jETI platformy. |
Návaznosti | |
---|---|
GA201/06/1338, projekt VaV | Název: Automatizovaná verifikace softwaru |
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1ET408050503, projekt VaV | Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 19. 9. 2024 08:00