Many-core on-the-fly model checking of safety properties using GPUs

Research output: Contribution to journalArticleAcademicpeer-review

12 Citations (Scopus)
120 Downloads (Pure)

Abstract

Model checking is an automatic method to formally verify the correctness of a system specification. Such model checking specifications can be viewed as implicit descriptions of a large directed graph or state space, which, for most model checking operations, needs to be analysed. However, construction or on-the-fly exploration of the state space is computationally intensive and often can be prohibitive in practical applications. In this work, we present techniques to perform graph generation and exploration using general purpose graphics processors (GPUs). GPUs have been successfully applied in multiple application domains to drastically speed up computations. We explain the limitations involved when trying to achieve efficient state space exploration with GPUs and present solutions how to overcome these. We discuss the possible approaches involving related work and propose an alternative, using a new hash table approach for GPUs. As input, we consider models that can be represented by a fixed number of communicating finite-state Labelled Transition Systems. This means that we assume that all variables used in a model range over finite data domains. Additionally, we show how our exploration technique can be extended to detect deadlocks and check safety properties on-the-fly. Experimental evaluations with our prototype implementations show significant speed-ups compared to the established sequential counterparts. Keywords: GPU; Model checking; Safety properties; Graph search; Refinement
Original languageEnglish
Pages (from-to)169-185
Number of pages17
JournalInternational Journal on Software Tools for Technology Transfer
Volume18
Issue number2
DOIs
Publication statusPublished - 1 Apr 2016

Fingerprint

Dive into the research topics of 'Many-core on-the-fly model checking of safety properties using GPUs'. Together they form a unique fingerprint.

Cite this