On theorem prover-based testing

被引：18

作者：

Brucker, Achim D. ^{[1
]}

Wolff, Burkhart ^{[2
]}

机构：

[1] SAP Res, D-76131 Karlsruhe, Germany

[2] Univ Paris 11, F-91405 Orsay, France

来源：

FORMAL ASPECTS OF COMPUTING | 2013年 / 25卷 / 05期

关键词：

Test case generation; Domain partitioning; Test sequence; Theorem proving; HOL-TestGen; TEST-GENERATION; HOL; COVERAGE;

D O I：

10.1007/s00165-012-0222-y

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, Testgen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.

引用

页码：683 / 721

页数：39

共 51 条

[11]

Boyapati C., 2002, Software Engineering Notes, V27, P123, DOI 10.1145/566171.566191

[12]

Brucker Achim D., 2010, Proceedings of the Third IEEE International Conference on Software Testing, Verification and Validation (ICST 2010), P345, DOI 10.1109/ICST.2010.50

[13]

Brucker A. D., 2005, LECT NOTES COMPUTER, V3997

[14]

Brucker AD, 2008, LECT NOTES COMPUT SC, V5047, P103, DOI 10.1007/978-3-540-68524-1_9

[15]

Brucker AD, 2007, LECT NOTES COMPUT SC, V4454, P149

[16]

Brucker AD, 2009, LECT NOTES COMPUT SC, V5503, P417

[17] An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP plus [J].