Towards Automatic Verification of Structural Code-Coverage Preservation

Raimund Kirner

Vienna University of Technology, Vienna, Austria

Embedded Systems are ofen used in safty-critical environments. Thus, thorough testing of them is mandatory. To achieve a required structural code-coverage criterion it is beneficial to derive the test data at a higher program-representation level than machine code. Higher program-representation levels include, besides the source-code level, languages of domain-specific modeling environments with automatic code generation. This enables for a testing framework with automatic test-data generation to achieve high retargetability. Within the project "Sustaining Entire Code-Coverage on Code Optimization" (SECCO) we address the challenge of ensuring that the structural code coverage achieved at a higher program representation level is preserved during the code generations and code transformations down to machine code [1,2]. We define the formal properties that have to be fulfilled by a code transformation to guarantee preservation of structural code coverage. Based on these properties we will formalize code transformations to automatically prove whether a given code coverage preserves the code coverage of interest.  


[1]     Raimund Kirner. Towards preserving model coverage and structural code coverage. Submitted for publication, 2008. Research report 49/2008.
[2]     Raimund Kirner and Susanne Kandl. Test coverage analysis and preservation for requirements-based testing of safety-critical systems. ERCIM News, (75):40-41, Oct. 2008.


Univ. Assistent Dr. Raimund Kirner received his Master's degree and his PhD degree at the Vienna University of Technology (TU Vienna) in 2000 respectively 2003. During this time he has been working as a research and teaching assistant at the Institut für Technische Informatik at TU Vienna. The main focus of Kirner's research is worst-case execution time analysis of real-time programs, including compiler support and design methodologies to make systems predictable. He has published several papers on WCET analysis and was involved in two projects funded by the European Commission (SETTA, NEXT TTA). From 2003-2005 Raimund Kirner has worked on the FIT-IT project MoDECS, and from 2005-2007 he worked on the FIT-IT project TeDES, both funded by the Federal Ministry of Transport, Innovation, and Technology (BMVIT). Currently, Raimund Kirner is principal investigator of the following projects: "Compiler-Support for Timing Analysis" (COSTA), "Formal Timing Analysis Suite" (FORTAS), and "Sustaining Entire Code-Coverage on Code Optimization" (SECCO). He is a member of the IEEE Computer Society, the ACM, and the Austrian Computer Society (OCG).

Contact Raimund at:

Dr. Raimund Kirner
Institute of Computer Engineering
Vienna University of Technology
A-1040 Vienna, Austria
raimund at