mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
Identifiers
URN: urn:nbn:se:mdh:diva-14661OAI: oai:DiVA.org:mdh-14661DiVA: diva2:529906
Subject / course
Computer Science
Presentation
2012-06-14, Gamma, Högskoleplan 1, Västerås, 08:15 (Swedish)
Uppsok
Technology
Supervisors
Examiners
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)200 downloads
File information
File name FULLTEXT01.pdfFile size 246 kBChecksum SHA-512
32386e11b30e8e7b078269eecfda7f88ff9ae3cfd4d5bec88a9479121f79acc91d1565f2d70a75d45ba51abe454e6b3553e0ca338639875bc60d16cc104c23e7
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: 200 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: 178 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf