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.

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

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