Bachelor and Master Theses

Title: Model-based Testing on Generated C Code
Subject: Computer Science
Level: Advanced
Description: Automated test case generation for covering logic structure of Function Block Diagrams is an ongoing research activity being conducted at Software Testing Laboratory at MDH. In [1], we proposed an approach which utilised Uppaal model-checker for generating tests. In this thesis, we would like to explore possibilities of using CMBC or CPAChecker model checkers. The motivation for exploring these specific tools comes from the fact that their listed as top software model checkers in the 3rd International Competition on Software Verification (SV-COMP'14) [2].

References:
Automated Test Generation using Model-Checking: An Industrial Evaluation (Nov 2014) Eduard Paul Enoiu, Adnan Causevic, Thomas Ostrand, Elaine Weyuker, Daniel Sundmark, Paul Pettersson International Journal on Software Tools for Technology Transfer (STTT)
http://sv-comp.sosy-lab.org/2014/results/
Prel. end date: 2015-06-07
Presentation date: 2015-06-04
Student: Athanasios Stratis ass14003@student.mdh.se
IDT supervisor: Adnan Causevic
adnan.causevic@mdh.se, 021-101689
Examinator: Kristina Lundqvist
Kristina Lundqvist
kristina.lundqvist@mdh.se, +46 (0)21 101428

Rapport och bilagor

Size

Senaste uppdatering

TR1737.pdf

1425201

2015-06-01, 09:02


  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2017.10.14