FAST: Formal specification driven test harness generation

Full coverage testing is commonly perceived as a mission impossible because software is more complex than ever and produces vast space to cover. This paper introduces a novel approach which uses ACSL formal specifications to define and reach test coverage, especially in the sense of data coverage. B...

Full description

Saved in:
Bibliographic Details
Main Authors: Jiong Gong, Yun Wang, Haihao Shen, Xu Deng, Wei Wang, Xiangning Ma
Format: Conference Proceeding
Language:English
Subjects:
ACSL
Data Coverage
Formal Specification Language
Formal specifications
Generators
Manuals
Mission critical systems
Resource management
Software
Test Generation
Test Harness
Testing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Full coverage testing is commonly perceived as a mission impossible because software is more complex than ever and produces vast space to cover. This paper introduces a novel approach which uses ACSL formal specifications to define and reach test coverage, especially in the sense of data coverage. Based on this approach, we create a tool chain named FAST which can automatically generate test harness code and verify program's correctness, turning formal specification and static verification into coverage definition and dynamic testing. FAST ensures completeness of test coverage and result checking by leveraging the formal specifications. We have applied this methodology and tool chain to a real-world mission critical software project that requires high quality standard. Our practice shows using FAST detects extra code bugs that escape from other validation methods such as manually-written tests and random/fuzz tests. It also costs much less human efforts with higher bug detection rate and higher code and data coverage.
DOI:10.1109/MEMCOD.2012.6292298