Parallel Model Checking and the FMICS-jETI Platform

BARNAT, Jiri, Lubos BRIM and 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, p. 330-339. ISBN 0-7695-2895-3.

Basic information

• Original name: Parallel Model Checking and the FMICS-jETI Platform
• Name in Czech: Paralelní ověřování modelů a platforma FMICS-jETI
• Authors: BARNAT, Jiri (203 Czech Republic), Lubos BRIM (203 Czech Republic, guarantor) and Martin LEUCKER (276 Germany).
• Edition: Los Alamitos, Proceedings Twelfth IEEE International Conference on Engineering of Complex Computer Systems, p. 330-339, 10 pp. 2007.
• Publisher: IEEE Computer Society

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: New Zealand
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/07:00019460
• Organization unit: Faculty of Informatics
• ISBN: 0-7695-2895-3
• UT WoS: 000248574000034
• Keywords in English: Parallel Model Checking; FMICS-jETI platform
• Tags: FMICS-jETI platform, parallel model checking
• Tags: International impact, Reviewed

Abstract

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.

Abstract (in Czech)

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.

Links

• GA201/06/1338, research and development project: Name: Automatizovaná verifikace softwaru

Investor: Czech Science Foundation, Automated software verification

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science