Journal of Advances in Information Technology, Vol 3, No 1 (2012), 10-20, Feb 2012
doi:10.4304/jait.3.1.10-20

iiOSProTrain: An Interactive Intelligent Online System for Programming Training

Tho Thanh Quan, Phung H Nguyen, Thang H Bui, Thuan Dinh Le, An Nhu Nguyen, Duc L.N. Hoang, Vu Huu Nguyen, Binh Thien Nguyen

Abstract


Programming is a crucial skill which is required to be mastered for students on all disciplines of the Computer Science field. For novice students, they always desire explanation and help for all errors encountered in their own solutions. With the recent advancement of Internet technologies, online tutoring systems are increasingly considered. Various systems and applications have been introduced for teaching programming. In this paper, we introduce a tutoring system known as iiOSProTrain (interactive intelligent Online System for Programming Training) for teaching students programming. In iiOSProTrain, we employ two popular formal methods, which are theorem proving and model checking, for verifying students’ works and giving them detailed feedback. The usage of formal methods renders our system the following advantages, as compared to similar systems. First, iiOSProTrain can give an absolute confirmation on the correctness of the submitted programs. More importantly, iiOSProTrain adopts the concept of structured error-flow to give students traceable feedbacks on their mistakes, thus allowing them to track and correct the logic errors in a flexible and convenient manner. Currently, iiOSProTrain is deployed at Faculty of Computer Science and Engineering, Ho Chi Minh University of Technology, Vietnam for teaching first year students on programming methodologies.


Keywords


intelligent tutoring systems; programming training; formal methods; program verification; courter-examples; error-flows

References


[1] The Joint Task Force: Computing Curricula 2001, Computer Science, ACM, 2001.

[2] Al-Hammadi A.H., Ahmed R.E, and Zualkernan I., Adoption of E-Learning Technology for Anti-Money Laundering Training, Journal of Advances in Information Technology, Vol. 1, No. 2, 2010.
http://dx.doi.org/10.4304/jait.1.2.73-83

[3] Tagga, A. Modern Sociology. Lahore: Tagga & Sons Publishers, 2007.

[4] H. Dobler, R. Ramler and K. Wolfmaier. “A Study of Tool Support for the Evaluation of Programming Exercises”, Computer Aided Systems Theory – EUROCAST 2007, Springer, 2007.

[5] Affleck, G. and Smith, T, “Identifying a need for web-based course support”. Proc. Conference of the Australasian Society for Computers in Learning in Tertiary Education, Brisbane, Australia, Online, 1999

[6] M. Jazayeri. “The Education of a Software Engineer”. Proceedings of 19th IEEE Conference on Automated Software Engineering, Linz, Austria, 2004.
http://dx.doi.org/10.1109/ASE.2004.1342718

[7] Ben-Ari, M. “Constructivism in Computer Science Education”. Journal of Computers in Mathematics & Science Teaching 20(1): 2001, 24-73.

[8] Sanders, D. and Hartman, J. “Assessing the quality of programs”: A topic for the CS2 course. Proc, 1987.

[9] Norcio, A. F. “Human Memory Processes for Comprehending Computer Programs”. Proc. IEEE Systems, Man and Cybernetics Society, Cambridge, Massachusetts, 1980, 974-977, IEEE.

[10] Mengel, S. And Yerramilli, V. “A Case Study Of The Static Analysis Of the Quality Of Novice Student Programs”. Proc. Thirtieth SIGCSE technical symposium on Computer science education, New Orleans, Louisiana, United States, 13:78-82, 1999.

[11] K.E. Wiegers. Peer Reviews in Software, Addison Wesley, London, UK, 2002.

[12] A. Spillner, T. Linz, H. Schaefer. Software Testing Foundations, dpunkt, 2006.

[13] D. A. Duffy, “Principles of Automated Theorem Proving”, John Wiley & Sons, 1991.

[14] E. M. Clarke and E. A. Emerson. “Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic”. Logic of Programs: 52-71, 1981

[15] Carnegie Mellon University. Alice Education Software, available at http://www.cmu.edu/corporate/news/2007/features/alice.shtml

[16] A. Moreno, N. Myller and E. Sutinen. “JECO, a Collaborative Learning Tool for Programming”, Proceedings of 2004 IEEE Symposium on Visual Languages and Human Centric Computing: 261-263, 2004.
http://dx.doi.org/10.1109/VLHCC.2004.33

[17] Deek, F. and Mchugh, J. “A survey and critical analysis of Tools for Learning Programming”. Journal of Computer Science Education, 8(2): 130-178, 1998.
http://dx.doi.org/10.1076/csed.8.2.130.3820

[18] Halstead, M. H. “Elements of software science”, Elsevier, New York, 1977.

[19] Mccabe, T. J. “A Complexity Measure”. IEEE Transactions on Software Engineering, 2(4): 308-320, 1976.
http://dx.doi.org/10.1109/TSE.1976.233837

[20] Leach, R. J. “Using metrics to evaluate student programs”. ACM SIGCSE Bulletin, 27(2): 41-43, 1995.
http://dx.doi.org/10.1145/201998.202010

[21] Jackson, D. “A software system for grading student computer programs”. Proc. the twenty-eighth SIGCSE technical symposium on Computer science education, San Jose, California, United States 28: 335-339, ACM Press, 1997.

[22] Schorsch, T. “CAP: An automated self-assessment tool to check Pascal programs for syntax, logic and style errors”. Proc. The twenty-sixth SIGCSE technical. 1995.

[23] Hristova, M., Misra, A., Rutter, M. and Mercuri, R. “Identifying and Correcting Java Programming Errors for Introductory Computer Science Students”. Proc.the 34th SIGCSE technical symposium on Computer science education, Reno, Nevada, USA, 34:153-156, ACM Press. 2003.

[24] Reek, K. A. “The TRY system -or- how to avoid testing student programs”. Proc. The twentieth SIGCSE technical symposium on Computer science education, Louisville, Kentucky, United States, 21:112-116, ACM Press New York, NY, USA, 1989.

[25] Joy, M., Griffiths, N., and Boyatt, R. “The boss online submission and assessment system”. J. Educ. Resour. Comput. 5, 3 (Sep. 2005), 2.

[26] CourseMaster: School of Computer Science & IT, The University of Nottingham, UK. http://www.cs.nott.ac.uk/CourseMaster/cm_com/index.html . Accessed 2002

[27] Sun, Y. and Jones, E. L. “Specification-driven automated testing of GUI-based Java programs”. In Proceedings of the 42nd Annual Southeast Regional Conference (Huntsville, Alabama, April 02 - 03, 2004). ACM-SE 42. ACM, New York, NY, 140-145.

[28] Man Yu Feng; Mcallister, A.; "A Tool for Automated GUI Program Grading," Frontiers in Education Conference, 36th Annual, vol., no., pp.7-12, 27-31 Oct. 2006

[29] Fu, X., Peltsverger, B., Qian, K., Tao, L., and Liu, J. "APOGEE: automated project grading and instant feedback system for web based computing”. SIGCSE Bull. 40, 1 (Feb. 2008), 77-81
http://dx.doi.org/10.1145/1352322.1352163

[30] Sztipanovits, M., Qian, K., and Fu, X. “The automated web application testing (AWAT) system”. In Proceedings of the 46th Annual Southeast Regional Conference on XX (Auburn, Alabama, March 28 - 29, 2008). ACM-SE 46. ACM, New York, NY, 88-93

[31] Truong, N., Bancroft, P., and Roe, P. 2003. A web based environment for learning to program. In Proceedings of the 26th Australasian Computer Science Conference - Volume 16 (Adelaide, Australia). M. J. Oudshoorn, Ed. ACSC, vol. 35. Australian Computer Society, Darlinghurst, Australia, 255-264.

[32] Truong, N., Roe, P., and Bancroft, P. “Static analysis of students' Java programs”. In Proceedings of the Sixth Conference on Australasian Computing Education - Volume 30 (Dunedin, New Zealand). R. Lister and A. Young, Eds. ACM International Conference Proceeding Series, vol. 57. Australian Computer Society, Darlinghurst, Australia, 317-325, 2004.

[33] Truong, N., Roe, P., and Bancroft, P. “Automated feedback for "fill in the gap" programming exercises”. In Proceedings of the 7th Australasian Conference on Computing Education - Volume 42 (Newcastle, New South Wales, Australia). A. Young and D. Tolhurst, Eds. ACM International Conference Proceeding Series, vol. 106. Australian Computer Society, Darlinghurst, Australia, 117-126, 2005.

[34] M Huth and M. Ryanl, Logic In Computer Science: Modeling And Reasoning About Systems, Cambridge University Press, 1999.

[35] Z3: An Efficient SMT Solver, available at http://research.microsoft.com/en-us/um/redmond/projects/z3/

[36] Detlefs, D., Nelson, G., and Saxe, J. B. “Simplify: a theorem prover for program checking”. J. ACM 52, 3 (May. 2005), 365-473.

[37] The Coq Proof Assistant, available at http://www.lix.polytechnique.fr/coq/

[38] Isabelle, available at http://www.cl.cam.ac.uk/research/hvg/Isabelle/

[39] The Alt-Ergo Theorem Prover, available at http://alt-ergo.lri.fr/

[40] Redlog, avaliable at http://redlog.dolzmann.de/

[41] Frama-C, available at http://frama-c.com/

[42] Why: a software verification platform, available at: http://why.lri.fr/.

[43] HIP Overview, available at http://loris-7.ddns.comp.nus.edu.sg/~project/hip/index.html

[44] Flanagan, C. and Qadeer, S. “Predicate abstraction for software verification”. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, Oregon, January 16 - 18, 2002). POPL '02. ACM, New York, NY, 191-202.

[45] Clarke, E.M.; Kurshan, R.P.; "Computer-aided verification," Spectrum, IEEE, vol.33, no.6, pp.61-67, Jun 1996.

[46] Spin – Formal Verification, available at http://spinroot.com/

[47] Java PathFinder, available at http://babelfish.arc.nasa.gov/trac/jpf

[48] NuSMV – a new symbolic model checker, available at http://nusmv.fbk.eu/

[49] J. Sun, Y. Liu, J.S. Dong and J. Pang. “PAT: Towards Flexible Verification under Fairness”. In Proceedings of the 21th International Conference on Computer Aided Verification (CAV 2009), Grenoble, France, June, 2009.

[50] P. Baudin, J. C. Filliâtre, C. Marché, B. Monate, Y. Moy and V. Prevosto. “ACSL: ANSI/ISO C Specification Language”, preliminary design (version 1.4). October 2008.

[51] G. C. Necula, S. Mcpeak, S. P. Rahul and W. Weimer. “CIL: Intermediate language and tools for analysis and transformation of C programs”. In International Conference on Compiler Construction, pp. 213-228, 2002.
http://dx.doi.org/10.1007/3-540-45937-5_16

[52] The PROMELA language, available at http://www.dai-arc.polito.it/dai-arc/manual/tools/jcat/main/node168.html

[53] Quan, T.T.; Hoang, D.L.N.; Nguyen, B.T.; Nguyen, A.N.; Tran, Q.D.; Nguyen, P.H.; Bui, T.H.; Do, A.T.; Huynh, L.V.; Doan, N.T.; Huynh, N.T.; Nguyen, T.D.; Nguyen, T.T.; Nguyen, V.H.; 9-11 June 2010 "MAFSE: A Model-Based Framework for Software Verification," Secure Software Integration and Reliability Improvement Companion (SSIRI-C), 2010 Fourth International Conference on, vol., no., pp.150-156.

[54] Quan T.T., Hoang D.L.N., Nguyen.V.H. and Nguyen P.H. 2010., “Model–based Generation of Structured Error–Flows in Imperative Programs”, In Proceedings of International Conference on Advanced Computing and Applications (ACOMP 2010).

[55] JESSIE plugin, available at http://frama-c.cea.fr/jessie.html

[56] Separation Logic: A Logic for Shared Mutable Data Structures John Reynolds. Proceedings of LICS 2002. pp55-74

[57] P. Godefroid, Using partial orders to improve automatic verification methods, Computer-Aided Verification, LNCS 531, pp. 176-185, Springer, 1991.


Full Text: PDF


Journal of Advances in Information Technology (JAIT, ISSN 1798-2340)

Copyright @ 2006-2014 by ACADEMY PUBLISHER – All rights reserved.