Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Model checking of multicore software using CBMC
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2012 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Computers have been key subsystems in various complex systems. As computers are adapted into various fields, hardware and software are increasing in size and complexity. It is evident that parallel computing is the way to solve large scale complex information technology problems.

Engineers designing hardware and software are required to verify the system for correctness. As system's size and complexity increases, it is difficult to perform manual system verification. Model checking converts a hardware or software solution into temporal logic and uses solvers to assert on properties of solution. A Bounded Model Checker can verify properties of program/logic within bounded limits. CBMC is a Bounded Model Checker for ANSI-C and C++ programs.

Thesis work is done considering an Ericsson's multicore platform as case study, which uses DSP-C as programming language. DSP-C is a set of language extensions on ISO C programming language. These extensions allow programmers to describe features of Digital Signal Processor (DSP). The work includes extending CBMC to support DSP-C, identifying Bounded Model Checking (BMC) techniques to cope-up with concurrency of Ericsson's multicore Digital Signal Processor (DSP) platform and implementing new features in CBMC to detect issues with Ericsson's parallel software.

Place, publisher, year, edition, pages
2012.
Series
IT, 12 047
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-182169OAI: oai:DiVA.org:uu-182169DiVA: diva2:558633
Educational program
Masters Programme in Embedded Systems
Uppsok
Technology
Supervisors
Examiners
Available from: 2012-10-04 Created: 2012-10-04 Last updated: 2012-10-04Bibliographically approved

Open Access in DiVA

fulltext(712 kB)529 downloads
File information
File name FULLTEXT01.pdfFile size 712 kBChecksum SHA-512
4013b761b061afd9210fea4575594836e6a702c6920d6f6b96378343fe8eba5e1094dc1ea578339b94dc8f1bb1945662bf4803613571771f70e203dc990e8c2a
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 529 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

urn-nbn

Altmetric score

urn-nbn
Total: 1059 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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