Parallel Model Checking and the FMICS-jETI Platform

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 µ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 the FMICS-jETI platform.

• Type: Conference
• Year: 2007
• Where: ICECCS
• Authors: Jiri Barnat, Lubos Brim, Martin Leucker
• Keywords: Enumerative Model Checking, Hardware, ICECCS 2007, Model Checking, Time Temporal Logic