Change search
ReferencesLink to record
Permanent link

Direct link
GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks
Mälardalen University, School of Innovation, Design and Engineering.
Mälardalen University, School of Innovation, Design and Engineering.
2012 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
Abstract [en]

Efficient model checking is important in order to make this type of software verification useful for systems that are complex in their structure. If a system is too large or complex then model checking does not simply scale, i.e., it could take too much time to verify the system. This is one strong argument for focusing on making model checking faster. Another interesting aim is to make model checking so fast that it can be used for predicting scheduling decisions for real-time schedulers at runtime. This of course requires the model checking to complete within a order of milliseconds or even microseconds. The aim is set very high but the results of this thesis will at least give a hint on whether this seems possible or not. The magic card for (maybe) making this possible is called Graphics Processing Unit (GPU). This thesis will investigate if and how a model checking algorithm can be ported and executed on a GPU. Modern GPU architectures offers a high degree of processing power since they are equipped with up to 1000 (NVIDIA GTX 590) or 3000 (NVIDIA Tesla K10) processor cores. The drawback is that they offer poor thread-communication possibilities and memory caches compared to CPU. This makes it very difficult to port CPU programs to GPUs.The example model (system) used in this thesis represents a real-time task scheduler that can schedule up to three periodic self-suspending tasks. The aim is to verify, i.e., find a feasible schedule for these tasks, and do it as fast as possible with the help of the GPU.

Place, publisher, year, edition, pages
2012. , 40 p.
Keyword [en]
GPU, Model Checking, Verification, CUDA, STS, Tree search, GPGPU, Periodic Self-Suspending Tasks, Real-Time, Scheduling, Timed automata
National Category
Computer Systems
URN: urn:nbn:se:mdh:diva-14661OAI: diva2:529906
Subject / course
Computer Science
2012-06-14, Gamma, Högskoleplan 1, Västerås, 08:15 (Swedish)
Available from: 2012-07-16 Created: 2012-05-31 Last updated: 2012-07-16Bibliographically approved

Open Access in DiVA

GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks(246 kB)181 downloads
File information
File name FULLTEXT01.pdfFile size 246 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Liberg, TimMåhl, Per-Erik
By organisation
School of Innovation, Design and Engineering
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 181 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: 134 hits
ReferencesLink to record
Permanent link

Direct link