Symbolic simulation for debugging and analysis of REKO models using KLEE
Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
The verification of embedded software plays an important role in the design process of dependable and/or real-time systems. Testing remains an important means to validate desired system operation and offers accurate results (as we are examining the actual system and not a model thereof). However, coming up with test cases that stress possible errors is a difficult and time-consuming task. To this end, automatic test case generation offers an attractive solution. This thesis is based on the expansion of the REKO models validation, being REKO a component-based software which supports building system models for resource-constrained embedded systems based on Concurrent Reactive Objects and Components. The use of KLEE has been studied in order to generate test cases revealing both common errors (arithmetic and pointer dereferencing) and giving high code coverage (exciting feasible execution paths) in the existing REKO models. Furthermore, framework has been developed which automatically produce test that can be used to perform execution time measurements based on the KLEE tests.
Place, publisher, year, edition, pages
2013. , 46 p.
IdentifiersURN: urn:nbn:se:ltu:diva-42898Local ID: 0d939770-45c8-4b58-a67a-fe8529ff7e47OAI: oai:DiVA.org:ltu-42898DiVA: diva2:1016124
Subject / course
Student thesis, at least 30 credits
Computer Science and Engineering, master's level
Validerat; 20130619 (global_studentproject_submitter)2016-10-042016-10-04Bibliographically approved