USING FORMAL METHODS FOR TEST CASE GENERATION ACCORDING TO TRANSITION-BASED COVERAGE CRITERIA

(Received: 2015-09-15, Revised: 2015-11-01 , Accepted: 2015-11-08)

Authors Ahmad A. Saifan, Wafa Bani Mustafa,

Keywords #Formal method #Perfect developer #Test case generation #Cruise control system (CCS).

Abstract Formal methods play an important role in increasing the quality, reliability, robustness and effectiveness of the software. Also, the uses of formal methods, especially in safety-critical systems, help in the early detection of software errors and failures which will reduce the cost and effort involved in software testing. The aim of this paper is to prove the role and effectiveness of formal specification for the cruise control system (CCS) as a case study. A CCS formal model is built using Perfect formal specification language, and its correctness is validated using the Perfect Developer toolset. We develop a software testing tool in order to generate test cases using three different algorithms. These test cases are evaluated to improve their coverage and effectiveness. The results show that random test case generation with full restriction algorithm is the best in its coverage results; the average of the path coverage is 77.78% and the average of the state coverage is 100%. Finally, our experimental results show that Perfect formal specification language is appropriate to specify CCS which is one of the most safety-critical software systems, so the process of detecting all future possible cases becomes easier.

References

[1] J. R. Abrial, Modeling in Event-B: System and Software Engineering, 1st Edition, Cambridge University Press, New York, NY, USA, 2010.

[2] P. Ammann and J. Offutt, "Introduction to Software Testing," 2008, Available at: http://www.cs.gmu.edu/~offutt/softwaretest/.

[3] J. Atlee and J. Gannon, "State-Based Model Checking of Event-Driven System Requirements," IEEE Transactions on Software Engineering, vol. 19, issue 1, pp. 24-40, Jan. 1993.

[4] T. Bultan and C. L. Heitmeyer, "Applying Infinite State Model Checking and Other Analysis Techniques to Tabular Requirements Specifications of Safety-Critical Systems," Design Automation for Embedded Systems, vol. 12, issue 1, pp. 97-137, June 2008. URL http://dx.doi.org/10.1007/s10617-008-9014-2.

[5] G. Carter and R. Monahan, "Software Refinement with Perfect Developer," 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM’05), pp. 363-373, 2005.

[6] Y. Chen, "Generation of Test Cases for Concurrent Software Systems Based on Data-Flow-Oriented Specifications," IEEE 2011 First ACIS/JNU International Conference on Computers, Networks, Systems and Industrial Engineering (CNSI), pp. 170-177, 23-25 May.

[7] D. Crocker, "Teaching Formal Methods with Perfect Developer," 2003, http://www.eschertech.com/papers/teaching_formal_methods.pdf.

[8] D. Crocker and J. Carlton, "Verification of C Programs Using Automated Reasoning," in: SEFM '07: Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods, 2007 IEEE Computer Society, Washington, DC, USA, pp. 7-14.

[9] G. Fraser and A. Gargantini, "An Evaluation of Model Checkers for Specification Based Test Case Generation," 2013 IEEE 6th International Conference on Software Testing, Verification and Validation, pp. 41-50, Denver, Colorado, 1-4 April 2009.

[10] C. Heitmeyer, J. Kirby and B. Labaw, "Tools for Formal Specification, Verification and Validation of Requirements," Proceedings of the IEEE 12th Annual Conference on Computer Assurance (COMPASS '97), pp. 35-47, 16-19 June 1997.

[11] A. Iliasov, A. Romanovsky and F. Dotti, "Structuring Specifications with Modes," 4th IEEE Latin-American Symposium on Dependable Computing (LADC '09), PP. 81-88, 1-4 Sept. 2009.

[12] S. Kanwal and N. Zafar, "Formal Model of Automated Teller Machine System Using Z Notation," IEEE International Conference on Emerging Technologies (ICET 2007), pp. 131-136, 12-13 Nov. 2007.

[13] A. Krupp, O. Lundkvist, T. Schattkowsky and C. Snook, "The Adaptive Cruise Controller Case Study Visualization, Validation and Temporal Verification," in UML-B System Specification for Proven Electronic Design, 9 Dec. 2004, Kluwer Academic Publishers 2005.

[14] S. Liu, "Utilizing Test Case Generation to Inspect Formal Specifications for Completeness and Feasibility," 9th IEEE International Symposium on High-Assurance Systems Engineering (HASE'05), pp. 349-356, 2005.

[15] S. Liu and S. A. Nakajima, "A Decompositional Approach to Automatic Test Case Generation Based on Formal Specifications," IEEE 2010 4th International Conference on Secure Software Integration and Reliability Improvement (SSIRI), pp. 147-155, Singapore, 9-11 June 2010.

[16] Q. Malik, J. Lilius and L. Laibinis, "Scenario-Based Test Case Generation Using Event-B Models," IEEE 1st International Conference of Advances in System Testing and Validation Lifecycle (VALID '09), pp. 31-37, 20-25 Sept. 2009.

[17] D. Mery and N. K. Singh, "Critical Systems Development Methodology Using Formal Techniques," in: Proceedings of the 3rd Symposium on Information and Communication Technology (SoICT '12), pp. 3-12, Viet Nam, 23 – 24 August 2012. URL http://doi.acm.org/10.1145/2350716.2350720.

[18] A. Mishra, M. Rao, C. Cu, V. Rao, Y. Jeppu and N. Murthy, "An Auto-Review Tool for Model-Based Testing of Safety-Critical Systems," in: Proceedings of the 2013 International Workshop on Joining AcadeMiA and Industry Contributions to Testing Automation, JAMAICA 2013, pp. 47-52, ACM, New York, NY, USA, 2013.

[19] Y. Nakatsugawa, P. Kurita and K. Araki, "A Framework for Formal Specification Considering Review and Specification-Based Testing," 2010 IEEE Region 10 Conference-TENCON 2010, pp. 2444 – 2448, ISBN: 978-1-4244-6889-8, Fukuoka, 21-24 Nov. 2010.

[20] J. Offutt, Y. Xiong and S. Liu, "Criteria for Generating Specification-Based Tests," 5th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'99), pp. 119-131, Las Vegas, Nevada, USA, 18-21 October 1999.

[21] I. Sommerville, Software Engineering, 9th Edition. Addison-Wesley, Haelow, England, 2010.

[22] C. Tian, S. Liu and S. Nakajima, "Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates," Proceedings of the 2011 IEEE 4th International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011), pp. 304-309.

[23] G. Tim, "Object-Z to Perfect Developer", 2007, Available at: http://www.doc.ic.ac.uk/~tk106/ObjectZ_project.pdf.

[24] A. Yasmeen, K. M. Feigh, G. Gelman and E. L. Gunter, "Formal Analysis of Safety-Critical System Simulations," in: Proceedings of the 2nd International Conference on Application and Theory of Automation in Command and Control Systems (ATACCS '12), pp.71-81, London, UK, 29-31 May 2012.

[25] D. You and S. Rayadurgam, "Practical Aspects of Building a Constrained Random Test Framework for Safety Critical Embedded Systems," in: Proceedings of the 1st International Workshop on Modern Software Engineering Methods for Industrial Automation (MoSEMInA 2014), pp. 17-25, ACM, New York, NY, USA, 2014.

[26] P. Nilsson, O. Hussien, Y. Chen, A. Balkan, M. Rungger, A. D. Ames, J. Grizzle, N. Ozay, H. Peng and P. Tabuada, "Preliminary Results on Correct-by-Construction Control Software Synthesis for Adaptive Cruise Control," Proc. 53rd IEEE Conference on Decision and Control (CDC), Dec. 2014.

[27] Y. Zhao, "Intuitive Representations for Temporal Logic Formulas," in Proc. of Forum on Specification and Design Language (FDL’03), pp. 405–413, Frankfurt, Germany, September 2003.

[28] A. Gotlieb, B. Botella and M. Rueher, "Automatic Test Data Generation Using Constraint Solving Techniques," in Proceedings of the 1998 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '98), Will Tracz (Ed.), pp. 53-62, FL, USA, 02 – 04 March 1998.

[29] J. Yan, Z. Li, Y. Yuan, W. Sun and J. Zhang, "BPEL4WS Unit Testing: Test Case Generation Using a Concurrent Path Analysis Approach," IEEE 17th International Symposium on Software Reliability Engineering (ISSRE ’06), pp. 75 – 84, 7-10 Nov. 2006.

[30] S. Jehan, I. Pill and F. Wotawa, "BPEL Integration Testing," 18th International Conference on Fundamental Approaches to Software Engineering (FASE), pp. 69-83, London, UK, 11-18 April 2015.

[31] M. Utting and B. Legeard, Practical Model-Based Testing: A Tools Approach, Morgan Kaufman Publishers Inc. San Francisco, CA, USA, 2007, ISBN:0123725011 9780080466484.