Разработка транслятора кода из C в Promela, как компонента интеллектуальной обучающей системы для обучения программированию

Представленная работа посвящена разработке транслятора с языка Си в язык Promela для автоматической верификации программ студентов, обучающихся программированию. Целью является создание инструмента, позволяющего проверять корректность промежуточных шагов выполнения программы с использованием Model Checking. Предложенный транслятор ориентирован на последовательные программы с единственной функцией main, работающие с целыми числами и массивами. Он анализирует C-код студента, требования к диапазонам входных данных и иерархическую LTL-спецификацию (дерево целей), описывающую ожидаемое поведение программы. В процессе трансляции используется clang для построения синтаксического дерева, а также создаются дополнительные переменные для отслеживания обращений к массивам. Сгенерированный Promela-код содержит объявления переменных, главный процесс, включающий недетерминированный ввод переменных и транслированный C-код, а также, блок LTL-свойств. Полученная Promela-модель верифицируется с помощью Spin на LTL-свойствах, заданных преподавателем. В случае обнаружения нарушения генерируется контрпример, демонстрирующий трассу выполнения программы с ошибкой. Результатом работы является консольная утилита на Python, которая генерирует .pml файл с Promela-кодом и LTL-свойствами, а также .json файл с размеченным деревом целей и контрпримером. В дальнейшем планируется автоматизировать генерацию LTL-свойств из описания требований на естественном языке и генерировать подсказки для студентов на основе контрпримеров.

1. Рудник П.Б., Зинина Т.С., Акиндинова Н.В. и др. Цифровая трансформация: эффекты и риски в новых условиях. Москва: ИСИЭЗ ВШЭ; 2024. 156 с.

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. Сычев О.А., Терехов Г.В. Инструменты помощи автору регулярных выражений для тестовых вопросов в СДО Moodle. Открытое образование. 2016;(3):43–50. 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