Change search
ReferencesLink to record
Permanent link

Direct link
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. , 44 p.
Keyword [en]
model-checker, cpachecker, testing
National Category
Computer Systems
URN: urn:nbn:se:mdh:diva-28381OAI: diva2:823332
Subject / course
Computer Science
Available from: 2015-06-30 Created: 2015-06-18 Last updated: 2015-06-30Bibliographically approved

Open Access in DiVA

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

By organisation
School of Innovation, Design and Engineering
Computer Systems

Search outside of DiVA

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

Direct link