Multi-core model checking algorithm development
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...
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Final Year Project |
| Language: | English |
| Published: |
2015
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/10356/62857 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Nanyang Technological University |
| Language: | English |
| Summary: | 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. |
|---|