Concurrency testing using symbolic path finder

  • Authors

    • Bidush Kumar Sahoo
    • Mitrabinda Ray
    2018-03-11
    https://doi.org/10.14419/ijet.v7i2.6.10782
  • Coverage Criteria, Java Path Finder, Model Checker, Symbolic Execution, Symbolic Path Finder.

  • Concurrent programs have specific features such as italic communication, synchronization and nondeterministic behavior that make the testing activity complex. The objective is to find various types of concurrent defects. In this paper, we have used a model checking tool called Symbolic Path Finder (SPF) which is the upgradation of Java Path Finder (JPF) for concurrent testing. SPF is used for generating the test cases to check concurrent defects such as deadlock, race condition etc. SPF generates symbolic execution tree of the given code which is used as an input for test case generation. The execution is done for finding the test cases in concurrent program where number of threads is operating together with the concurrent defects. The test cases show the type of concurrent defects in the respective line number of the source code.

     

     

  • References

    1. [1] Asadollah, Sara Abbaspour, Hans Hansson, Daniel Sundmark, and Sigrid Eldh., “Towards classification of concurrency bugs based on observable propertiesâ€, (2015) In Complex Faults and Failures in Large Software Systems (COUFLESS), IEEE/ACM 1st International Workshop on, pp. 41-47, IEEE.

      [2] Melo, Silvana M., Paulo SL Souza, and Simone RS Souza., “Towards an empirical study design for concurrent software testingâ€, (2016) In Software Engineering for High Performance Computing in Computational Science and Engineering (SE-HPCCSE), Fourth International Workshop on, pp. 49-49. IEEE.

      [3] Choudhary, Ankit, Shan Lu, and Michael Pradel., “Efficient detection of thread safety violations via coverage-guided generation of concurrent testsâ€, (2017) In Proceedings of the 39th International Conference on Software Engineering, pp. 266-277. IEEE Press.

      [4] Yu, Tingting, Wei Wen, Xue Han, and Jane Huffman Hayes., Predicting Testability of Concurrent Programs, (2016) In Software Testing, Verification and Validation (ICST), IEEE International Conference on, pp. 168-179. IEEE.

      [5] Chen, F., Rosu, G., “Parametric and sliced causalityâ€, (2007) In: Computer Aided Verification, Springer, pp. 240–253, LNCS 4590.

      [6] Serbanuta, T.F., Chen, F., Rosu, G., “Maximal causal models for multithreaded systemsâ€, (2008) Technical Report UIUCDCS-R-2008-3017, University of Illinois at Urbana-Champaign.

      [7] Bianchi, Francesco, Alessandro Margara, and Mauro Pezze., “A Survey of Recent Trends in Testing Concurrent Software Systemsâ€, (2017) IEEE Transactions on Software Engineering.

      [8] Melo, Silvana M., Paulo SL Souza, and Simone RS Souza., “Towards an empirical study design for concurrent software testingâ€, (2016) In Software Engineering for High Performance Computing in Computational Science and Engineering (SE-HPCCSE), Fourth International Workshop on, pp. 49-49. IEEE.

      [9] Guo, Shengjian, Markus Kusano, and Chao Wang., “Conc-iSE: Incremental symbolic execution of concurrent softwareâ€, (2016) In Automated Software Engineering (ASE), 31st IEEE/ACM International Conference on, pp. 531-542. IEEE.

      [10] Lahiri, S., Qadeer, S., “Back to the future: revisiting precise program verification using SMT solversâ€, (2008) In: Principles of Programming Languages, ACM, pp. 171–182.

      [11] Dutertre, B., de Moura, L., “A fast linear-arithmetic solver for dpll(t)â€, (2006) In: Computer Aided Verification, Springer, pp. 81–94, LNCS 4144.

      [12] Metzler, Patrick, Habib Saissi, Péter Bokor, and Neeraj Suri., “Quick verification of concurrent programs by iteratively relaxed schedulingâ€, (2017) In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, pp. 776-781. IEEE Press.

      [13] Wang, C., Yang, Z., Kahlon, V., Gupta, A., “Peephole partial order reductionâ€, (2008) In: Tools and Algorithms for Construction and Analysis of Systems, Springer, pp. 382–396 LNCS 4963.

      [14] Terragni, Valerio, and Shing-Chi Cheung., “Coverage-driven test code generation for concurrent classesâ€, (2016) In Software Engineering (ICSE), IEEE/ACM 38th International Conference on, pp. 1121-1132. IEEE.

      [15] Musuvathi, M., Qadeer, S., “CHESS: Systematic stress testing of concurrent softwareâ€, (2006) In: Logic-Based Program Synthesis and Transformation, Springer, pp. 15–16 LNCS 4407.

      [16] Lal, A., Reps, T.W., “Reducing concurrent analysis under a context bound to sequential analysisâ€, (2008) In: Computer Aided Verification, Springer, pp. 37–53, LNCS 5123.

      [17] Wang, Jie, Wensheng Dou, Yu Gao, Chushu Gao, Feng Qin, Kang Yin, and Jun Wei., “A comprehensive study on real world concurrency bugs in Node. Jsâ€, (2017) In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, pp. 520-531. IEEE Press.

  • Downloads

  • How to Cite

    Kumar Sahoo, B., & Ray, M. (2018). Concurrency testing using symbolic path finder. International Journal of Engineering & Technology, 7(2.6), 275-282. https://doi.org/10.14419/ijet.v7i2.6.10782