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

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

V originále

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.

Č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