Please use this identifier to cite or link to this item:
Title: Multi-core model checking algorithm development
Authors: Xu, Yi
Keywords: DRNTU::Engineering::Computer science and engineering
DRNTU::Engineering::Computer science and engineering
Issue Date: 2015
Abstract: Model checking is an automatic technique for verifying finite state systems. Strongly Connected Components (SCC) detection is one of the major approaches for LTL Model Checking, which is suitable for fairness assumption. Currently, Tarjan’s Algorithm is a widely used Depth-first search (DFS) process to deal with the SCC detection problem, which has been implemented as sequential algorithms in many tools, e.g. Process Analysis Toolkit (PAT). However, It always costs a lot of time with large-scale system models. In my project, I improve the performance of Tarjan’s algorithm by implementing and optimizing the concurrent Tarjan’s algorithm described in Gavin’s Paper. Different from the algorithm in that paper, I optimize the concurrent Tarjan’s algorithm to build an approach that can support the on-the-fly LTL model checking with fairness assumption in PAT.
Rights: Nanyang Technological University
Fulltext Permission: restricted
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Student Reports (FYP/IA/PA/PI)

Files in This Item:
File Description SizeFormat 
Xu Yi - FYP Report.pdf
  Restricted Access
8.44 MBAdobe PDFView/Open

Page view(s)

checked on Sep 29, 2020


checked on Sep 29, 2020

Google ScholarTM


Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.