Метод формальной верификации программ для виртуальной лаборатории «Машина Поста»


https://doi.org/10.15217/issnl684-8853.2018.2.104

Полный текст:


Аннотация

Введение: формальная верификация программ в символьном виде позволяет в автоматическом режиме осуществлять оценку практических навыков обучающихся при наличии неразрешимого множества верных ответов, что существенно облегчает разработку программных компонентов, используемых для оценки. Цель: разработка нового метода формальной верификации программ в символьном виде для виртуальной лаборатории «Машина Поста». Результаты: разработан новый метод формальной верификации программ в символьном виде для виртуальной лаборатории «Машина Поста». Сформулированы основные принципы и примеры формирования программ для машины Поста и методы их символьной формализации. Рассмотрены различные задачи использования математических операций с представленными на ленте машины числами в унарном коде, в частности: прибавление единицы к числу, сложение и умножение двух чисел, остановка работы программы в определенной конфигурации ленты машины, переход к новой конфигурации машины от первоначально заданной. Рассмотренных задач достаточно для формирования у обучающихся базовых практических навыков алгоритмизации, а символьное представление решения таких задач позволит упростить разработку оценивающих средств виртуальной лаборатории «Машина Поста» и осуществлять контроль формирования данных навыков в автоматическом режиме. Представлена концепция внедрения разработанного метода верификации программ в уже существующие обучающие информационные системы. Практическая значимость: разработанный метод формальной верификации программ для виртуальной лаборатории «Машина Поста» позволяет осуществлять оценку практических навыков алгоритмизации задач у обучающихся и упростить разработку виртуальных лабораторий путем уменьшения затрат на формирование тестовых наборов данных для проведения оценивающих мероприятий.

Об авторе

А. В. Лямин
Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики
Россия


Список литературы

1. Аврунин О. Г., Крук О. Я., Носова Т. В., Семенец В. В. Технические аспекты разработки виртуальных лабораторных работ по техническим дисциплинам // Открытое образование. 2008. № 3. С. 11-17.

2. Васильев В. Н., Лисицына Л. С., Лямин А. В. Сетевая технология проведения вступительных испытаний по информатике в режиме on-line // Использование информационно-коммуникационных технологий в процессе оценки качества образования: сб. науч. тр. 2008. С. 55-70.

3. Kay J., Reimann P., Diebold E., Kummerfeld B. MOOCs: So Many Learners, So Much Potential.. // IEEE Intelligent Systems. 2013. Vol. 28(3). P. 70-77. doi: 10.1109/MIS.2013.66

4. Zang X., Iqbal S., Zhu Y., Riaz M. S., Abbas G., Zhao J. Are MOOCs Advancing as Predicted by IEEE CS 2022 Report? // Intern. Conf. on Proc. of the Systems Informatics, Modelling and Simulation (SIMS). 2016. P. 49-55. doi: 10.1109/SIMS.2016.14

5. Stuchlikova L., Kosa A. Massive Open Online Courses - Challenges and Solutions in Engineering Education // IEEE 11th Intern. Conf. on Emerging eLearning Technologies and Applications (ICETA). 2013. P. 359-364. doi: 10.1109/ICETA.2013.6674459

6. Djeghloud H., Larakeb M., Bentounsi A. Virtual Labs of Conventional Electric Machines // Intern. Conf. on Interactive Mobile and Computer Aided Learning (IMCL). 2012. P. 52-57. doi: 10.1109/IMCL.2012.6396450

7. Magyar Z., Zakova K. Using SciLab for Building of Virtual Lab // 9th Intern. Conf. on Information Technology Based Higher Education and Training (ITHET). 2010. P. 280-283. doi: 10.1109/ITHET.2010.5480084

8. Hristov G., Zahariev P., Bencheva N., Ivanov I. Designing the Next Generation of Virtual Learning Environments - Virtual Laboratory with Remote Access to Real Telecommunication Devices // Proc. of the 24th EAEEIE Annual Conf. (EAEEIE). 2013. P. 139-144. doi: 10.1109/EAEEIE.2013.6576517

9. Moritz D., Willems C., Goderbauer M., Moeller P., Meinel C. Enhancing a Virtual Security Lab with a Private Cloud Framework // IEEE Intern. Conf. on Teaching, Assessment and Learning for Engineering (TALE). 2013. P. 314-320. doi: 10.1109/TALE.2013. 6654452

10. Ахи А. А., Станкевич А. С., Шалыто А. А. Автоматические методы модификации решений для тестирования проверяющих программ // Научнотехнический вестник информационных технологий, механики и оптики. 2012. № 1(77). С. 81-85.

11. Ефимчик Е. А. Автоматическое построение заданий для проверки навыков выполнения операций над множествами // Новые информационные технологии в образовании: материалы междунар. науч.-практ. конф. 2013. С. 278-281.

12. Lisitsyna L. S., Efimchik E. A., Izgareva S. A. RLCP-compatible Virtual Laboratories with 3d-mod-els and Demonstration Mode: Development and Application in e-learning // Smart Innovation, Systems and Technologies. 2018. Vol. 75. P. 75-81. doi: https://doi.org/10.1007/978-3-319-59451-4_8

13. Efimchik E. A., Cherepovskaya E. N., Lyamin A. V. RLCP-Compatible Virtual Laboratories in Computer Science // Smart Innovation, Systems and Technologies. 2016. P. 303-314. doi: https://doi.org/10.1007/978-3-319-39690-3_27

14. Efimchik E. A., Chezhin M. S., Lyamin A. V., Ru-sak A. V. Using Automaton Model to Determine the Complexity of Algorithmic Problems for Virtual Laboratories // 9th Intern. Conf. on Application of Information and Communication Technologies (AICT 2015). 2015. P. 541-545. doi: 10.1109/ICAICT.2015.7338619

15. Sandya M. Competence Possessed by Engineering Professionals in Regard to the Prevailing Trends and Worldwide Attitudes Towards Engineering Education // IEEE Intern. Conf. on Engineering Education: Innovative Practices and Future Trends (AICERA). 2012. P. 1-6.

16. Post E. L. Finite Combinatory Processes-Formulation 1 // The Journal of Symbolic Logic. 1936. Vol. 1. N 3. P. 103-105.

17. Вашенков О. Е., Лямин А. В. Методика формирования эталонных наборов входных и выходных данных для анализа результатов выполнения заданий с неразрешимым множеством правильных ответов // Научно-технический вестник информационных технологий, механики и оптики. 2009. № 3 (61). С. 99-105.


Дополнительные файлы

Для цитирования: Лямин А.В. Метод формальной верификации программ для виртуальной лаборатории «Машина Поста». Информационно-управляющие системы. 2018;93(2):104-114. https://doi.org/10.15217/issnl684-8853.2018.2.104

For citation: Lyamin A.V. Method of Formal Program Verification for Post Machine Virtua l Laboratory. Information and Control Systems. 2018;93(2):104-114. (In Russ.) https://doi.org/10.15217/issnl684-8853.2018.2.104

Просмотров: 32


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1684-8853 (Print)
ISSN 2541-8610 (Online)