ФОРМАЛЬНА МОДЕЛЬ ВЕРИФІКАЦІЇ ПЕРСОНАЛІЗОВАНИХ ОСВІТНІХ ТРАЄКТОРІЙ НА ОСНОВІ ALLOY.
Date
2026
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
У статті розглянуто проблему верифікації персоналізованих освітніх траєкторій у сучасній освітній інженерії в умовах цифровізації освітнього процесу. Обґрунтовано необхідність перевірки коректності навчальних маршрутів, сформованих з урахуванням індивідуальних освітніх потреб, попереднього досвіду, рівня підготовки та професійних цілей здобувачів освіти. Акцентовано увагу на тому, що ефе- ктивність персоналізованого навчання визначається не лише якістю проєктування індивідуальної тра- єкторії, а й можливістю її формальної перевірки на узгодженість, повноту та досяжність результатів.
Запропоновано формальну модель, реалізовану засобами мови специфікації Alloy, яка дозволяє пере- віряти відповідність набутих навичок вимогам кар'єрної мети. У межах моделі визначено ключові сут- ності, зокрема здобувача освіти, навчальні дисципліни, набуті та необхідні навички, а також профе- сійні орієнтації, і формалізовано зв’язки між ними. Запроваджено систему інваріантів і обмежень, що забезпечують перевірку коректності освітніх траєкторій, включаючи наявність визначеної кар’єрної мети, змістовність навчальних компонентів і відповідність результатів навчання вимогам професійної діяльності. Модель забезпечує динамічну перевірку досяжності освітніх результатів шляхом аналізу змін у наборі набутих навичок на різних етапах навчання. Це дає змогу виявляти потенційні помилки у формуванні траєкторій, оцінювати ефективність алгоритмів рекомендації навчальних дисциплін і підтверджувати досяжність визначених цілей. Отримані результати засвідчують, що застосування фо- рмального підходу сприяє підвищенню валідності персоналізованого навчання, обґрунтованості осві- тніх рішень та ефективності адаптивних освітніх систем. Перспективи подальших досліджень пов’язані з розширенням системи обмежень, урахуванням невизначеності даних і вдосконаленням ме- ханізмів адаптації освітніх траєкторій. The article addresses the problem of verification of personalized educational trajectories in modern educa- tional engineering under the conditions of digitalization of the educational process. The necessity of verifying the correctness of learning pathways formed with regard to individual educational needs, prior experience, level of training, and professional goals of learners is substantiated. It is emphasized that the effectiveness of personalized learning is determined not only by the quality of individual trajectory design but also by the possibility of its formal verification in terms of consistency, completeness, and attainability of results.
A formal model implemented using the Alloy specification language is proposed, which enables verification of the correspondence between acquired skills and the requirements of a career goal. Within the model, key entities are defined, including the learner, educational subjects, acquired and required skills, as well as pro- fessional aspirations, and the relationships between them are formalized. A system of invariants and con- straints is introduced to ensure the correctness of educational trajectories, including the presence of a defined career goal, the meaningfulness of educational components, and the alignment of learning outcomes with professional requirements. The model provides dynamic verification of the attainability of educational results through the analysis of changes in the set of acquired skills at different stages of learning. This makes it possible to identify potential errors in trajectory construction, evaluate the effectiveness of course recommen- dation algorithms, and confirm the attainability of defined goals. The obtained results demonstrate that the application of a formal approach contributes to increasing the validity of personalized learning, the soundness of educational decisions, and the efficiency of adaptive educational systems. Prospects for further research are related to extending the system of constraints, taking into account data uncertainty, and improving mech- anisms for adapting educational trajectories.
Description
Полторацький М. Ю., Волянюк А. С. Формальна модель верифікації персоналізованих освітніх траєкторій на основі ALLOY. Проблеми програмування. 2026. № 2. С. 87–96.
Keywords
персоналізоване навчання, освітня траєкторія, верифікація, освітня інженерія, адапти- вність, навички, кар'єрна мета, алгоритм, модель, навчальний курс, personalized learning, educational trajectory, verification, educational engineering, adaptability, skills, career goal, algorithm, model, course.