In this thesis, we propose a scheme to verify the SYN-sequence generated in dynamic testing of concurrent software and provide the theoretic fundations. We first translate the SYN-sequence into the model of reachability graph or partial order graph. Then the model as well as the specifications a feed into the NuSMV model checker. If the model satisfies the specifications, the NuSMV will return true and we are confident that the SYN-sequence also satisfies the specifications. If the model doesn’t satisfy the specifications, the NuSMV will report the falsity along with an counterexample. In this case, users can debug or modify the concurrent programs according to this counterexample.
We can apply one out of three different models, i.e. stateful or general model, stateless model and partial order model. It depends on the type of specifications and the problem size. If the specifications are stateful, they can be expressed in Type I and only stateful model can be used. Otherwise, specifications involving stateless properties can expressed in Type II or III. Specifications in Type II, or stateless specifications, can be verified on both stateful and stateless models. Even so, stateless model is better choice since the better performance in large problem size. Specifications in Type III are more difficult to be expressed and can be verified only on partial order model. It request the user to be equipped with entire knowledge to write the correct expression. Unfortunately, when the problem size is too large such as to confront the state space explosion, only the partial order model can be adopted. None the less, since the size of specifications in Type III is usually larger than stateless specifications, the performance of partial order model is not guaranteed to be always better than that of stateless model.
The experimental result shows that a systematic verification of SYN-sequence is feasible.
Reference
REFERENCES
[1] Charles E Mcdowell and David P. Helmold, “Debugging Concurrent Programs,”
ACM Computing Surveys, Volume 21, Issue 4, December 1989.
[2] K.C. Tai and Richard H. Carver, “Testing of Distributed Programs,” Chapter 33 in Parallel and Distributed Computing Handbook, editor A. Y. Zomaya, McGraw-Hill, 1996.
[3] Anne Dinning, “A Survey of Synchronization Methods for Parallel Computers,”
IEEE Computer, July 1989.
[4] Abraham Silberschatz, Peter Baer Galvin, and Greg Gagne, “Operating System Concepts,” John Wiley & Sons, ISBN: 0471417432, 6th edition (June 26, 2001).
[5] D. Helmbold and D. Luckham, “Debugging Ada tasking programs,” IEEE Software, Volume 2, Number 2, 66-74, 1985.
[6] K. C. Tai, “Testing of concurrent software,” Proc. of the 13th Annual International Computer Software and Applications Conference, pp. 62-64, 1989.
[7] Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999, ISBN 0-262-03270-8.
[8] Logic in Computer Science: Modelling and Reasoning About Systems, Michael Huth and Mark Ryan, Cambridge University Press, 2004.
[9] Holzmann, G.: The model checker SPIN. IEEE Trans. Software Engineering 23(5) (1997) 279–295
[10] Musuvathi, M., Park, D., Chou, A., Engler, D., L. Dill, D.: CMC: A pragmatic approach to model checking real code. In: OSDI 02: Operating Systems Design and Implementation (2002) 75–88
[11] Java PathFinder, http://javapathfinder.sourceforge.net/.
[12] MAGIC website, http://www.cs.cmu.edu/~chaki/magic.
[13] S. Chaki, J. Ouaknine, K. Yorav, and E. M. Clarke, “Automated compositional abstraction refinement for concurrent C programs,” In Proceedings of SoftMC 03.
ENTCS 89(3), 2003.
[14] W. Richards Adrion, Martha A. Branstad, and John C. Cherniavsky, “Validation, Verification, and Testing of Computer Software,” ACM Computing Surveys, Volume 14, Issue 2, June 1982.
[15] Roger S. Pressman, Software Engineering (A practitioner's approach), 5th edition, 2000, Mc Graw-Hill Education, ISBN 978-0071181822.
[16] Gwan-Hwan Hwang, “A Systematic Parallel Testing Method for Concurrent
Programs. Master Thesis,” Institute of Computer Science and Information Engineer, National Chiao-Tung University, Taiwan, 1993.
[17] G. H. Hwang, K. C. Tai, and T.L. Huang, “Reachability Testing: An Approach To Testing Concurrent Software,” International Journal of Software Engineering and Knowledge Eng., 5, 4, (Dec. 1995), 493-510.
[18] Gwan-Hwan Hwang and Che-Sheng Lin, “Dynamic Effective Testing: An Approach to Testing Concurrent Programs,” Technical Report, National Taiwan Normal University, 2008. http://www.csie.ntnu.edu.tw/~ghhwang/ DET2008.pdf.
[19] Thomas J. LeBlanc and John M. Mellor-Crummey, “Debugging Parallel Programs with Instant Replay,” IEEE Transactions on Computers, C-36(4), pp. 471-482, April 1987.
[20] Che-Sheng Lin and Gwan-Hwan Hwang, “Dynamic Termination Decision for Concurrent Programs with Busy-Waiting Loops,” Submitted to IEEE International Conference on Software Testing, Verification, and Validation, 2009 for publication.
[21] NuSMV, http://nusmv.irst.itc.it/.
[22] Stoller SD. Testing concurrent Java programs using randomized scheduling.
Proceedings of the 2nd Workshop on Runtime Verification (RV) (Electronic Notes in Theoretical Computer Science, vol. 70(4)). Elsevier: Amsterdam, 2002.
[23] Y. Ben-Asher, E. Farchi, Y. Eytani, “Heuristics for finding concurrent bugs,”
Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS 2003) PADTAD Workshop, April 2003. IEEE Computer Society Press:
Los Alamitos, CA, 2003.
[24] Edelstein O, Farchi E, Nir Y, Ratsaby G, Ur S. Multithreaded Java program test generation. IBM Systems Journal 2002; 41(1):111–125. Available at:
http://www.research.ibm.com/journal/sj/411/edelstein.html.
[25] Gwan-Hwan Hwang, Sheng-Jen Chang, and Huey-Der Chu, “Technology for Testing Nondeterministic Client/Server Database Applications,” IEEE Transaction on Software Engineering, Volume 30, Number 1, pp. 59-77, Jan., 2004.
[26] Kuo-Chung Tai, “Reachability Testing of Asynchronous Message-passing Programs,” Proceedings of the second International Workshop on Software Engineering for Parallel and Distributed Systems, 1997.
[27] Yu Lei and Kuo-Chung Tai, “Efficient Reachability Testing of Asynchronous Message-Passing Programs,” Proc. 8th IEEE Intl. Conf. on Engineering for Complex Computer Systems, pp. 35-44, Dec. 2002.
[28] Richard H. Carver and Yu Lei, “A General Model for Reachability Testing of Concurrent Programs,” ICFEM 2004, LNCS 3308, pp. 76-89, 2004.
[29] Yu Lei and Richard H. Carver, “Reachability Testing of Concurrent Programs,”
IEEE Transaction on Software Engineering, June 2006 (Vol. 32, No. 6), pp.
382-403.
[30] Yu Lei, Richard H. Carver, Raghu Kacker, and David Kung, “A combinatorial testing strategy for concurrent programs,” Software Testing, Verification &
Reliability ,Volume 17 , Issue 4 (December 2007) pages 207-225.
[31] Koushik Sen, Gul Agha, “Automated Systematic Testing of Open Distributed Programs,” Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, pp. 339-356.
[32] Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science. (1977) 46–57
[33] N. Rescher, A.U.: Temporal Logic. Springer (1971)
[34] Goldblatt, R.: Logic of time and computation. Technical report, CSLI Lecture Notes, no.7, Stanford University (1987)
[35] Kamp, J.: Tense Logic and the Theory of Order. PhD thesis, UCLA (1968)
[36] Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Logics of Programs.
Volume 193 of Lecture Notes in Computer Science., Springer (1985) 196–218 [37] Markey, N.: Temporal logic with past is exponentially more succinct. EATCS
Bulletin 79 (2003) 122–128
[38] Vardi, M.: A temporal fixpoint calculus. In: Proc. 15th ACM Symp. on Principles of Programming Languages. (1988) 250–259
[39] Keller, R.: Formal verification of parallel programs. Communications of the ACM 19 (1976) 371–384
[40] Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2002)
[41] Pratt, V.: A near-optimal method for reasoning about action. Journal of Computer and Systems Science 20(2) (1980) 231–254
[42] Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. Workshop on Logic of Programs. Volume 131 of Lecture Notes in Computer Science., Springer (1981) 52–71
[43] Queille, J., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Proc. 9th ACM Symp. on Principles of Programming Languages. Volume 137 of Lecture Notes in Computer Science., Springer (1982) 337–351
[44] Ben-Ari, M., Manna, Z., Pnueli, A.: The logic of nexttime. In: Proc. 8th ACM Symp. on Principles of Programming Languages. (1981) 164–176
[45] Lamport, L.: “Sometimes” is sometimes “not never” - on the temporal logic of programs. In: Proc. 7th ACM Symp. on Principles of Programming Languages.
(1980) 174–185
[46] Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In: Proc. 10th ACM Symp. on Principles of Programming Languages. (1983) 117–126
[47] Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languagues and Systems 8(2) (1986) 244–263
[48] Clarke, E., Grumberg, O.: Avoiding the state explosion problem in temporal logic model-checking algorithms. In: Proc. 16th ACM Symp. on Principles of Distributed Computing. (1987) 294–303
[49] Browne, M., Clarke, E., Dill, D., Mishra, B.: Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computing C-35 (1986) 1035–1044
[50] Clarke, E., Mishra, B.: Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science 38 (1985) 269–291
[51] Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking:
10 states and beyond. In: Proc. 5th IEEE Symp. on Logic in Computer Science.
(1990) 428–439
[52] Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking:
10 states and beyond. Information and Computation 98(2) (1992) 142–170 [53] McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers (1993) [54] Clarke, E.: The birth of model checking. In: 25 Years of Model Checking. Volume
5000 of Lecture Notes in Computer Science., Springer (2008) 1–26
[55] Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. on Principles of Programming Languages. (1985) 97–107
[56] CADP, http://www.inrialpes.fr/vasy/cadp/
[57] CHESS, http://research.microsoft.com/en-us/projects/CHESS/.
[58] ISP (In-situ Partial Order),
http://www.cs.utah.edu/formal_verification/ISP-release/
[59] Spin – Formal Verification, http://spinroot.com/spin/whatispin.html
[60] Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic
Model Checking. In: Computer Aided Verification. Volume 2404 of Lecture Notes in Computer Science., Springer (2002) 241–268
[61] H.Carver, R., Tai, K.-C.: Modern multithreading. John Wiley & Sons (2006) [62] Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans.
Software Eng, SE.3, 7 (1977) 125–143.
[63] Cavada, R., Cimatti, A., A. Jochim, C., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.4 User Manual. ITC-irst (2005)
[64] Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In:
Proc. 24th ACM Symp. on Principles of Programming Languages. (1997) 174–186