Citation: | TIAN Cong, LIU Shaoying, DUAN Zhenhua, “Test Case Generation from Conjunctions of Predicates with Model Checking,” Chinese Journal of Electronics, vol. 23, no. 2, pp. 271-277, 2014, |
M. Donat, "Automating formal specification-based testing", Proceedings of TAPSOFT'97, Lille, France: Springer-Verlag, pp.833-848, 1997.
|
S. Khurshid and D. Marinov, "TestEra: Specification-based testing of Java programs using SAT", Automated Software Engineering, Vol.11, No.4, pp.403-434, 2004.
|
M.G. Hinchey and J.P. Bowen (ed.). "Industrial-Strength Formal Methods in Practice", FACIT series. Springer-Verlag, London, UK, 1999.
|
J.Woodcock, P.G. Larsen, J. Bicarregui and J. Fitzgerald, "Formal methods: Practice and experience", ACM Computing Surveys, Vol.41, No.4, 2009.
|
J. Dick and A. Faivre, "Automating the generation and sequencing of test cases from model-based specifications", Proceedings of FME '93: Industrial-Strength Formal Methods, Odense, Denmark, Vol.670, pp.268-284, 1993.
|
S. Liu and S. Nakajima, "A decompositional approach to automatic test case generation based on formal specifications" 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010), pp.147-155, Singapore, 2010.
|
M. Utting and B. Legeard, Practical Model-Based Testing: A Tools Approach, Morgan Kaufmann, 2007.
|
Gerard J. Holzmann, "The model checker spin", IEEE Trans. on Software Engineering, Vol.23, No.5, pp.279-295, 1997.
|
E.M. Clarke and E.A. Emerson, "Desigh and syntesis of synchronization skeletons using branching time temporal logic", Logic of Programs 81, LNCS 131, Springer, pp.52-71, 1981.
|
J.P. Quielle and J. Sifakis, "Specification and verification of concurrent systems in CESAR", Proceedings of the 5th International Symposium on Programming, pp.337-350, 1981.
|
A. Pnueli, "The temporal logic of programs", Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, IEEE, New York, pp.46-67, 1977.
|
Markus Müller-Olm, David Schmidt and Bernhard Steffen, "Model-checking a tutorial introduction", Proceedings of SAS'99, LNCS 1694, pp.330-354, 1999.
|
Gerard J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, ISBN 0-321-22862-6, 2003.
|
S. Liu and S. Nakajima, "A "Vibration" method for automatically generating test cases based on formal specifications", APSECC 2011, pp.73-80, 2011.
|
J. Callahan, F. Schneider and S. Eastbrook, "Specificationbased testing using model-checking", Proc. 2nd SPIN Workshop, pp.193-207, 1996.
|
Hamon, L. de Moura and J. Rushby, "Automated test generation with SAL", CSL Technical Note, 2005.
|
D. Jackson, Software Abstractions, The MIT Press, 2006.
|
B. Dutertre and L. de Moura, "The YICES SMT Solver", http://yices.csl.sri.com/.
|
H. Lin and W. Zhang, "Model checking: Theories, techniques and applications", Acta Electronica Sinica, Vol.30, No.12A, pp.1907-1912, 2002.
|
C. Zhou, Z. Tao, D. Ding and L. Wang, "Bounded model checking for branching-time temporal logic", Chinese Journal of Electronics, Vol.15, No.4, pp.675-678, 2006.
|