Change search
ReferencesLink to record
Permanent link

Direct link
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
IT, 12 047
National Category
Engineering and Technology
URN: urn:nbn:se:uu:diva-182169OAI: diva2:558633
Educational program
Masters Programme in Embedded Systems
Available from: 2012-10-04 Created: 2012-10-04 Last updated: 2012-10-04Bibliographically approved

Open Access in DiVA

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

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

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

Direct link