This work focuses on the development of a C to Promela translator for the automated verification of programs written by programming students. The goal is to create a tool that allows checking the correctness of intermediate program execution steps using Model Checking. The proposed translator is geared towards sequential programs with a single main function, operating on integers and arrays. It analyzes the student’s C code, input data range requirements, and a hierarchical LTL specification (goal tree) that describes the expected program behavior. The translation process utilizes clang to construct the syntax tree and creates additional variables to track array accesses. The generated Promela code contains variable declarations, a main process that includes non-deterministic variable input and the translated C code, and an LTL properties block. The resulting Promela model is verified using Spin against the LTL properties specified by the instructor. If a violation is detected, a counterexample is generated, demonstrating the program execution trace containing the error. The result of this work is a command-line utility written in Python that generates a .pml file with Promela code and LTL properties, as well as a .json file containing the annotated goal tree and the counterexample. Future plans include automating the generation of LTL properties from natural language requirement descriptions and generating hints for students based on the counterexamples.
1. Rudnik P., Zinina T., Akindinova N., et al. Digital Transformation: Effects and Risks in New Conditions. Moscow: ISSEK HSE; 2024. 156 p. (In Russ.).
2. Rathore A.S., Arjaria S.K. Intelligent Tutoring System. In: Utilizing Educational Data Mining Techniques for Improved Learning: Emerging Research and Opportunities. Hershey PA: IGI Global; 2020. P. 121–144. https://doi.org/10.4018/978-1-7998-0010-1.ch006
3. Lewandowski G., Gutschow A., McCartney R., Sanders K., Shinners-Kennedy D. What Novice Programmers Don’t Know. In: ICER '05: Proceedings of the International Computing Education Research Workshop, 01–02 October 2005, Seattle, WA, USA. New York: Association for Computing Machinery; 2005. P. 1–12. https://doi.org/10.1145/1089786.1089787
4. Gerdes A., Heeren B., Jeuring J., Van Binsbergen Th. Ask-Elle: an Adaptable Programming Tutor for Haskell Giving Automated Feedback. International Journal of Artificial Intelligence in Education. 2017;27(1):65–100. https://doi.org/10.1007/s40593-015-0080-x
5. Kumar A.N. Solvelets: Tutors to Practice the Process of Programming. In: ITiCSE '22: Proceedings of the 27th ACM Conference on Innovation and Technology in Computer Science Education (ITiCSE 2022), 08–13 July 2022, Dublin, Ireland. New York: Association for Computing Machinery; 2022. P. 151–157. https://doi.org/10.1145/502718.3524811
6. Lazar T., Sadikov A., Bratko I. Rewrite Rules for Debugging Student Programs in Programming Tutors. IEEE Transactions on Learning Technologies. 2018;11(4):429–440. https://doi.org/10.1109/TLT.2017.2743701
7. Sychev O.A., Terehov G.V. Helping Tools for the Regular Expression Author for Test Questions in LMS Moodle. Open Education. 2016;(3):43–50. (In Russ.). https://doi.org/10.21686/1818-4243-2016-3-43-50
8. Verma A., Khatana A., Chaudhary S. A Comparative Study of Black Box Testing and White Box Testing. International Journal of Computer Sciences and Engineering. 2017;5(12):301–304. https://doi.org/10.26438/ijcse/v5i12.301304
9. MacIver D.R., Hatfield-Dodds Z., Contributors M. Hypothesis: A New Approach to Property-Based Testing. Journal of Open Source Software. 2019;4(43). https://doi.org/10.21105/joss.01891
10. Brain M., Polgreen E. A Pyramid Of (Formal) Software Verification. In: Formal Methods: 26th International Symposium, FM 2024: Proceedings, Part II, 09–13 September 2024, Milan, Italy. Cham: Springer; 2024. P. 393–419. https://doi.org/10.1007/978-3-031-71177-0_24
11. Clarke E.M., Grumberg O., Peled D.A. Model Checking. Cambridge: MIT Press; 2001. 314 p.
12. Clarke E.M., Emerson E.A., Sistla A.P. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems. 1986;8(2):244–263. https://doi.org/10.1145/5397.5399
13. Neumann R. Using Promela in a Fully Verified Executable LTL Model Checker. In: Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014: Revised Selected Papers, 17–18 July 2014, Vienna, Austria. Cham: Springer; 2014. P. 105–114. https://doi.org/10.1007/978-3-319-12154-3_7
14. Holzmann G.J., Ruys Th.C. Effective Bug Hunting with Spin and Modex. In: Model Checking Software: 12th International SPIN Workshop: Proceedings, 22–24 August 2005, San Francisco, CA, USA. Berlin; Heidelberg: Springer; 2005. P. 24. https://doi.org/10.1007/11537328_3
15. Kulyukin K., Litovkin D. An Approach to Formal Verification of Programs in Learning C Programming. In: Novel and Intelligent Digital Systems: Proceedings of the 4th International Conference (NiDS 2024), 25–27 September 2024, Athens, Greece. Cham: Springer; 2024. P. 443–447. https://doi.org/10.1007/978-3-031-73344-4_37
16. Jiang K., Jonsson B. Using SPIN to Model Check Concurrent Algorithms, using a translation from C to Promela. In: MCC '2009: Proceeding of the Second Swedish Workshop on Multi-Core Computing, 26–27 November 2009, Uppsala, Sweden. Uppsala: Department of Information Technology, Uppsala University; 2009. P. 67–69.
17. Wang X., Li G., Li Ch., Zhao L., Shu X. Automatic Generation of Specification from Natural Language Based on Temporal Logic. In: Structured Object-Oriented Formal Language and Method: 10th International Workshop, SOFL+MSVL 2020: Revised Selected Papers, 01 March 2021, Singapore. Cham: Springer; 2021. P. 154–171. https://doi.org/10.1007/978-3-030-77474-5_11
18. Kaleeswaran A.P., Nordmann A., Vogel Th., Grunske L. A Systematic Literature Review on Counterexample Explanation. Information and Software Technology. 2022;145. https://doi.org/10.1016/j.infsof.2021.106800
19. Feng L., Ghasemi M., Chang K.-W., Topcu U. Counterexamples for Robotic Planning Explained in Structured Language. In: 2018 IEEE International Conference on Robotics and Automation (ICRA), 21–25 May 2018, Brisbane, QLD, Australia. IEEE; 2018. P. 7292–7297. https://doi.org/10.1109/ICRA.2018.8460945
20. Nguyen T.Th.Th., Ogata K. A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker. In: 2017 International Conference on Software Analysis, Testing and Evolution (SATE), 03–04 November 2017, Harbin, China. IEEE; 2017. P. 53–62. https://doi.org/10.1109/SATE.2017.15
