Abstracting formal specifications to generate software tests via model checking
作者： P. Ammann , P.E. Black
关键词:
摘要: A recent method combines model checkers with specification-based mutation analysis to generate test cases from formal software specifications. However high-level specifications usually must be reduced make a checker feasible. We propose new reduction, parts of which can applied mechanically, soundly reduce some large, even infinite, state machines manageable pieces. Our work differs other in that we use the reduction for generating sets, as opposed typical goal analyzing properties. Consequently, have different criteria, and prove soundness rule. Informally rule is counterexamples are original specification. The changes machine temporal logic constraints checking specification avoid unsound cases. Java virtual stack an example generation.
sci-hub.se 参考文章(19)
D Richard Kuhn, Fault Classes and Error Detection in Specification Based Testing | NIST - 6140. ,(1998) , 10.6028/NIST.IR.6140
Phillip J. Windley, Michael D. Jones, Paul E. Black, Kelly M. Hall, Trent N. Larson, A Brief Introduction to Formal Methods ,(1996)
E. Clarke, O. Grumberg, D. Long, Verification Tools for Finite-State Concurrent Systems A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium. pp. 124- 175 ,(1993) , 10.1007/3-540-58043-3_19
Robert P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach ,(1995)
Ramesh Bharadwaj, Constance Heitmeyer, Verifying SCR Requirements Specifications Using State Exploration ,(1997)
P.E. Ammann, P.E. Black, A specification-based coverage metric to evaluate test sets high-assurance systems engineering. ,vol. 8, pp. 239- 248 ,(1999) , 10.1109/HASE.1999.809499
J. Rushby, Ubiquitous abstraction: a new approach for mechanized formal verification international conference on formal engineering methods. pp. 176- 178 ,(1998) , 10.1109/ICFEM.1998.730581
P.E. Black, K.M. Hall, M.D. Jones, T.N. Larson, P.J. Windley, A brief introduction to formal methods [hardware design] custom integrated circuits conference. pp. 377- 380 ,(1996) , 10.1109/CICC.1996.510579
P.E. Ammann, P.E. Black, W. Majurski, Using model checking to generate tests from specifications international conference on formal engineering methods. pp. 46- 54 ,(1998) , 10.1109/ICFEM.1998.730569
R.A. DeMillo, R.J. Lipton, F.G. Sayward, Hints on Test Data Selection: Help for the Practicing Programmer Computer. ,vol. 11, pp. 34- 41 ,(1978) , 10.1109/C-M.1978.218136