Change search
ReferencesLink to record
Permanent link

Direct link
Framework for Analyzing Highly Concurrent Algorithms in SPIN
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2011 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Human beings have gradually become dependent on computers, and more specifically, the software that they are working with. Most skillful programmers are working hard and spend much time testing or debugging their programs in order to make their software reliable.

Verification techniques have been developed to find bugs as much as possible in the early stages of development or implementation of the software. Model checking is one of the verification techniques which requires a simplified model of the system. It will test automatically whether this model accommodates the given system’s specification or not. One of the most successful tools for automatic verification is the SPIN Model Checker. It is a general tool for verifying the correctness of distributed software models, parallel algorithms and data structures. The input language of SPIN is Promela. Promela does not support some features such as pointer declarations, dynamic memory allocation, or garbage collection in order to be a simple modeling language and decrease the size of the state space.

This master thesis presents a framework in Promela for verifying safety and liveness properties of highly concurrent algorithms in the SPIN model checker. We present some macros in Promela which are independent from the specific behavior of a particular algorithm. These macros can be used in most concurrent algorithms which are verified by SPIN. In this work also we used some techniques for memory management. Some macros are created which do garbage collection and dynamic memory allocation themselves in our framework in a way that the behavior of the original algorithm is preserved maximally. We have applied our approach to some concurrent deque algorithms and evaluated the results.

Place, publisher, year, edition, pages
2011.
Series
IT, 11 017
Identifiers
URN: urn:nbn:se:uu:diva-152985OAI: oai:DiVA.org:uu-152985DiVA: diva2:414828
Uppsok
Technology
Supervisors
Examiners
Available from: 2011-05-04 Created: 2011-05-04 Last updated: 2011-05-04Bibliographically approved

Open Access in DiVA

fulltext(979 kB)346 downloads
File information
File name FULLTEXT01.pdfFile size 979 kBChecksum SHA-512
d2615f7d3ea6d19026ffa1442539e2b7adb590dee6f3c5c17cc66c5d59f50b6bfde70a140504818e82a0365b168cfa6f53a524f3ecb4fcef3e62c08908b90443
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 346 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 335 hits
ReferencesLink to record
Permanent link

Direct link