Digitala Vetenskapliga Arkivet

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-based Testing on Generated C Code
Mälardalen University, School of Innovation, Design and Engineering.
2015 (English)Independent thesis Advanced level (degree of Master (One Year)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

In this master thesis we investigated whether it is possible to use automatically generated C code from Function Block Diagram models as an input to the CPAchecker model checker in order to generate automated test cases. Function Block Diagram is a non-executable programming and modeling language. Consequently, we need to transform this language to an executable language that can be model checked. A tool that achieves this is the MITRAC tool, a proprietary development tool used in the embedded system domain, for engineering programmable logic controllers. The purpose of this research was to investigate to what extent the generated C code using MITRAC can be reused as an input to the CPAchecker tool for automated test case generation. In order to achieve this we needed to perform certain transformations steps on the existing code. In addition, necessary instrumentations were needed in order to trigger CPAtiger, an extension of CPAchecker which generates test cases, to achieve maximum condition coverage. We showed that by performing the required modifications it is feasible to reuse the generated C code as an input to CPAchecker tool. We also showed an approach for mapping the generated test cases with the actual Function Block Diagram. We performed mutation analysis in order to evaluate the quality of the generated test cases in terms of the number of injected faults they detect. Test case generation with CPAchecker could be improved in the future in terms of reducing the number of transformations and instrumentations that are currently needed. In order to achieve this we need to add to CPAchecker tool support for structures that are used in C, such as structs. Finally we can extend the type of logic coverage criteria we can use with CPAchecker by adding additional support of FQL language.

Place, publisher, year, edition, pages
2015. , p. 44
Keywords [en]
model-checker, cpachecker, testing
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-28381OAI: oai:DiVA.org:mdh-28381DiVA, id: diva2:823332
Subject / course
Computer Science
Supervisors
Examiners
Available from: 2015-06-30 Created: 2015-06-18 Last updated: 2015-06-30Bibliographically approved

Open Access in DiVA

fulltext(1392 kB)198 downloads
File information
File name FULLTEXT01.pdfFile size 1392 kBChecksum SHA-512
28473e546c2b61c12f8c29115152268f22eb0f1b7291143571728c1aa869dcbed70de617fb609490878e84f133c52f2ee0864ec81cd93dd4c49d2b4e539ea073
Type fulltextMimetype application/pdf

By organisation
School of Innovation, Design and Engineering
Computer Systems

Search outside of DiVA

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