Formal model for verification of personalized educational trajectories based on 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 educationa...

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2026
Автори:	Poltoratskyi, M.Yu., Volianiuk, A.S.
Формат:	Стаття
Мова:	Українська
Опубліковано:	PROBLEMS IN PROGRAMMING 2026
Теми:	personalized learning educational trajectory verification educational engineering adaptability skills career goal algorithm model course UDC 004.942:37.018.43
Онлайн доступ:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/1029
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Problems in programming
Завантажити файл:

Репозитарії

Problems in programming

_version_	1869381590309666816
author	Poltoratskyi, M.Yu. Volianiuk, A.S.
author_facet	Poltoratskyi, M.Yu. Volianiuk, A.S.
author_institution_txt_mv	[ { "author": "M.Yu. Poltoratskyi", "institution": "Kherson State University" }, { "author": "A.S. Volianiuk", "institution": "Kherson State University" } ]
author_sort	Poltoratskyi, M.Yu.
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
collection	OJS
datestamp_date	2026-06-29T10:43:50Z
description	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.Prombles in programming 2026; 2: 87-96
first_indexed	2026-06-30T01:00:10Z
format	Article
fulltext	87 Інформатизація науки і освіти © М.Ю. Полторацький, А.С. Волянюк, 2026 ISSN 1727-4907. Проблеми програмування. 2026. №2 https://pp.isofts.kiev.ua CC BY 4.0 УДК 004.942:37.018.43 https://doi.org/10.15407/pp2026.02.087 М.Ю. Полторацький, А.С. Волянюк ФОРМАЛЬНА МОДЕЛЬ ВЕРИФІКАЦІЇ ПЕРСОНАЛІЗОВАНИХ ОСВІТНІХ ТРАЄКТОРІЙ НА ОСНОВІ ALLOY У статті розглянуто проблему верифікації персоналізованих освітніх траєкторій у сучасній освітній інженерії в умовах цифровізації освітнього процесу. Обґрунтовано необхідність перевірки коректності навчальних маршрутів, сформованих з урахуванням індивідуальних освітніх потреб, попереднього досвіду, рівня підготовки та професійних цілей здобувачів освіти. Акцентовано увагу на тому, що ефе- ктивність персоналізованого навчання визначається не лише якістю проєктування індивідуальної тра- єкторії, а й можливістю її формальної перевірки на узгодженість, повноту та досяжність результатів. Запропоновано формальну модель, реалізовану засобами мови специфікації Alloy, яка дозволяє пере- віряти відповідність набутих навичок вимогам кар'єрної мети. У межах моделі визначено ключові сут- ності, зокрема здобувача освіти, навчальні дисципліни, набуті та необхідні навички, а також профе- сійні орієнтації, і формалізовано зв’язки між ними. Запроваджено систему інваріантів і обмежень, що забезпечують перевірку коректності освітніх траєкторій, включаючи наявність визначеної кар’єрної мети, змістовність навчальних компонентів і відповідність результатів навчання вимогам професійної діяльності. Модель забезпечує динамічну перевірку досяжності освітніх результатів шляхом аналізу змін у наборі набутих навичок на різних етапах навчання. Це дає змогу виявляти потенційні помилки у формуванні траєкторій, оцінювати ефективність алгоритмів рекомендації навчальних дисциплін і підтверджувати досяжність визначених цілей. Отримані результати засвідчують, що застосування фо- рмального підходу сприяє підвищенню валідності персоналізованого навчання, обґрунтованості осві- тніх рішень та ефективності адаптивних освітніх систем. Перспективи подальших досліджень пов’язані з розширенням системи обмежень, урахуванням невизначеності даних і вдосконаленням ме- ханізмів адаптації освітніх траєкторій. Ключові слова: персоналізоване навчання, освітня траєкторія, верифікація, освітня інженерія, адапти- вність, навички, кар'єрна мета, алгоритм, модель, навчальний курс M. Poltoratskyi, A. Volianiuk FORMAL MODEL FOR VERIFICATION OF PERSONALIZED EDUCATIONAL TRAJECTORIES BASED ON 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, p rior 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 invari ants 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. Key words: personalized learning, educational trajectory, verification, educational engineering, adaptability, skills, career goal, algorithm, model, course 88 Інформатизація науки і освіти Вступ Постановка проблеми. Персоналі- зоване навчання стало однією з провідних тенденцій сучасної освіти, набуваючи осо- бливої актуальності в контексті цифровіза- ції освітнього процесу. Його сутність поля- гає в адаптації навчання до індивідуальних потреб, інтересів, здібностей та цілей кож- ного учня. Такий підхід дозволяє відійти від стандартизованих моделей і створити умови для реалізації потенціалу кожного здобувача освіти. Розвиток інформаційно- комунікаційних технологій значною мірою сприяв поширенню персоналізації, зроби- вши її досяжною навіть у масштабних он- лайн- або змішаних формах навчання. Однією з ключових передумов ефек- тивної персоналізації є створення повного профілю здобувача освіти, який враховує його індивідуальні особливості, зокрема попередній досвід, рівень знань, ставлення до навчання та інтереси [1]. Такий профіль слугує основою для формування унікальної освітньої траєкторії, яка постійно оновлю- ється у відповідь на зміни в навчальних до- сягненнях і мотивації здобувача. У цьому контексті важливою складовою персоналі- зованого підходу є адаптивність, що реалі- зується через динамічне коригування змі- сту, темпу та форм подачі матеріалу [2, с. 872-875]. Саме адаптивні навчальні траєк- торії дозволяють забезпечити релевант- ність навчального досвіду на кожному етапі навчання, водночас підтримуючи інтерес та розвиток самостійності здобувача освіти. Важливою умовою реалізації персо- налізації є створення гнучких освітніх сере- довищ, які забезпечують здобувачам мож- ливість самостійно обирати темп, формат і зміст навчання відповідно до власних пот- реб і переваг. Це не лише сприяє підви- щенню мотивації та залученості, а й формує навички саморегуляції та відповідальності за результати власного навчання [3, с.501]. Однак, попри очевидні переваги, пе- рсоналізоване навчання стикається з рядом проблем, серед яких особливо актуальною є проблема перевірки коректності побудови індивідуальних освітніх траєкторій. Оскі- льки траєкторія формується автоматизо- вано на основі аналізу великої кількості да- них, існує ризик виникнення помилок у її конструюванні або у надмірному покла- данні на алгоритми, що не завжди здатні адекватно врахувати складну мотиваційно- особистісну структуру здобувача. Тоді пос- тає завдання забезпечити не лише техноло- гічну точність, а й валідність запропонова- них шляхів навчання. Це потребує розро- бки інструментів для верифікації освітніх траєкторій з урахуванням педагогічної до- цільності, гнучкості системи адаптації та ефективного зворотного зв'язку. Аналіз останніх досліджень і пуб- лікацій. Персоналізована освітня траєкто- рія на сьогодні є одним із ключових конце- птів сучасної освіти, що передбачає ство- рення унікального шляху навчання для ко- жного учня, побудованого відповідно до його здібностей, потреб, інтересів та цілей. У центрі цього підходу - особистість здобу- вача освіти, його активна участь у власному навчанні, а також створення умов для гнуч- кості та самостійності в здобутті знань. Науковиця Алєксєєва С. підкреслює, що «індивідуальна освітня траєкторія має стати дидактичною системою, в якій нав- чання здійснюється за індивідуальними програмами, змістом, формами, засобами, темпом та відповідними формами конт- ролю і оцінювання» [4, с. 5]. За її словами, головною метою такого підходу є максима- льний розвиток потенціалу кожного здобу- вача освіти через формування самостійно- сті, ініціативності, дослідницького стилю, творчості, впевненості та відповідального ставлення до праці. Особливої ваги індиві- дуальний підхід набуває в умовах нестабі- льності, як-от воєнний стан чи період після- воєнного відновлення, адже «цінність дида- ктичного алгоритму розроблення індивіду- альної освітньої траєкторії... у тому, що він підвищує мотивацію, розвиває вміння вчи- тися та допомагає учням досягати кращих результатів навчання» [4, с.6]. У контексті освітньої реформи в Ук- раїні індивідуалізація навчання розгляда- ється як необхідний крок до оновлення си- стеми освіти. Науковці Лавренова М., Ла- лак Н., Молнар Т. та Фенчак Л. зазначають, що «одним із найважливіших аспектів ре- формування системи освіти в Україні є ці- леспрямована та системна робота педагогів 89 Інформатизація науки і освіти над створенням індивідуальної освітньої траєкторії розвитку здобувача освіти як пе- рсонального шляху реалізації його особис- тісного потенціалу» [5, с.131]. Для втілення цього підходу необхідно переосмислити не лише зміст навчання, а й способи його ор- ганізації, форми контролю та критерії оці- нювання. Групою науковців під керівницт- вом Співаковського О. доведено, що вико- ристання ІКТ у збалансованій системі (фу- ндаментальна, інваріантна та варіантна складові здобуття освіти) впливає на конку- рентоспроможність випускників, що при- водить до капіталізації студентів як майбу- тніх спеціалістів, здатних інтегрувати свої знання в умовах мінливого соціального та кооперативного середовища [6]. Реалізація персоналізованої освіт- ньої траєкторії вимагає створення умов, за яких здобувачі освіти отримають можли- вість самостійно визначати зміст навчання, обирати індивідуальні цілі, підбирати ме- тоди та темпи засвоєння матеріалу, а також усвідомлювати та оцінювати власний пос- туп. Як зазначають дослідники, «учень зможе просуватись індивідуальною траєк- торією в тому випадку, якщо йому надава- тимуть такі можливості: визначати індиві- дуальний зміст вивчення навчальних пред- метів; ставити власні цілі у вивченні конк- ретної теми або розділу; вибирати оптима- льні форми та темпи навчання; застосову- вати ті способи навчання, що найбільш від- повідають його індивідуальним особливос- тям; рефлексивно усвідомлювати отримані результати, оцінювати і коригувати свою діяльність» [5, с.137]. Таким чином, персоналізована осві- тня траєкторія не лише сприяє розвитку особистості здобувача, а й трансформує саму логіку освітнього процесу до особис- тісно орієнтованого, гнучкого і динаміч- ного підходу, здатного відповідати викли- кам сучасності. На основі аналізу наукових джерел ми притримуємось думки, що персоналізо- ване навчання як інноваційна педагогічна парадигма вимагає не лише створення, а й постійної перевірки коректності індивідуа- льних освітніх траєкторій, що формуються для кожного здобувача освіти. Сучасні дослідження пропонують низку технологічних рішень цієї проблеми. Наприклад, у статті З. Папамітцоу [7] розг- лядається два підходи до формування та ве- рифікації індивідуальних освітніх маршру- тів у цифрових середовищах. Перший з них передбачає використання генетичних алго- ритмів, які дозволяють знайти оптимальні шляхи навчання, враховуючи індивідуальні освітні потреби. Цей підхід виявився ефек- тивним у генерації динамічних і релевант- них траєкторій, особливо в умовах онлайн- навчання, де гнучкість та адаптивність є критично важливими. Другий підхід базу- ється на застосуванні нейронних мереж, що формують рекомендації щодо подальших кроків у навчанні, адаптуючи траєкторії на основі аналізу освітньої поведінки учня. Обидва підходи підтримують автоматизо- ване ухвалення рішень, однак потребують постійного оновлення даних і уточнення моделей, аби гарантувати їхню педагогічну валідність [7]. Інший важливий напрям досліджень представлений у роботі Ковалюк Т., Кобець Н. та Дворник В. [8, с.115-128], де основний акцент зроблено на аналізі мотиваційних факторів як передумови формування інди- відуального освітнього шляху. Авторки ро- зробили інформаційну технологію, що до- зволяє формувати траєкторії на основі лате- нтно-семантичного аналізу мотиваційних листів здобувачів освіти, результатів опи- тувань щодо професійних інтересів та оці- нки поточного рівня знань. Отримані дані використовуються для побудови онтологій предметних галузей у вигляді тезаурусів, які виступають концептуальними моде- лями змісту навчання. У результаті створю- ється індивідуальний навчальний план, що поєднує особистісну мотивацію, профе- сійну спрямованість і рівень підготовки здобувача вищої освіти. Загалом розроблені алгоритмічні підходи та аналітичні інструменти значно розширюють можливості перевірки й адап- тації освітніх траєкторій, однак їхня ефек- тивність залежить від якості вхідних даних та здатності моделей адекватно відобра- жати складну структуру мотиваційно-цін- нісної сфери учня. Тому подальший розви- ток персоналізованого навчання потребує 90 Інформатизація науки і освіти інтеграції технологічної точності з педаго- гічною доцільністю, а також створення ме- ханізмів зворотного зв’язку, що дозволять коригувати траєкторії відповідно до змін в особистісному розвитку учня. Успішна ре- алізація цих завдань може забезпечити ви- соку ефективність персоналізованого під- ходу та його стійку інтеграцію в освітні си- стеми майбутнього. Мета дослідження. Метою статті є обґрунтування можливості ефективного за- стосування формальної мови моделювання Alloy для перевірки досяжності під час фо- рмування персоналізованих освітніх траєк- торій. Методологія дослідження. У попередніх публікаціях було запропоновано модель побудови персоналізованих освітніх траєк- торій із використанням технологій Semantic Web [9], розроблено RDF-модель [10] пер- соналізованого освітнього середовища за- собами мови Notation3 [11], а також сис- тему імплікаційних правил за допомогою мови N3 Logic Rules [12]. У статтi Полторацького М. та Кон- нової О. [13] представлено опис методів ва- лідації освітніх моделей на основі RDF і мови опису обмежень SHACL [14] та мови запитів SPARQL [15] для оцінки їхньої від- повідності сучасним вимогам ринку праці. На основі попередніх (зазначених вище) досліджень було вдосконалено мо- дель сучасного персоналізованого освіт- нього середовища, а також розроблено ал- горитми рекомендації курсів відповідно до кар'єрних уподобань здобувача вищої освіти. У цій статті основну увагу зосере- джено на розробці формальної моделі та пе- ревірці коректності запропонованого під- ходу до побудови персоналізованих освіт- ніх траєкторій із використанням мови спе- цифікації Alloy [16]. Результати дослідження. Опис моделi. У цьому розділі статті увагу зосере- джено на розробці формальної моделі та пе- ревірці коректності запропонованого під- ходу в статтi [16] за допомогою мови спе- цифікації Alloy. Сутностi в Alloy розглядаються як сигнатури. Отож Student - це сигнатура, яка має певний набір відношень, що можуть зв’язувати кожну сутнiсть з iншими. Да- вайте розглянемо сигнатуру Student деталь- ніше: abstract sig Student { acquiredSkills: set Skill, aspiresTo: set careerAspir, enrollTo: set Subject } Сутність Student - це абстрактна си- гнатура, яка має три відношення, що зв’язу- ються з множиною інших сутностей, а саме: - acquiredSkills — відношення, яке пов’язує здобувача освіти з множи- ною навичок, які він уже здобув. Це ті навички, якi необхiднi для запису на іншу дисципліну (освітню компо- ненту). Прикладом можуть бути “Основи програмної інженерії” та “Формальні методи програмного за- безпечення”; - aspiresTo — відношення, яке вказує на множину професійних цілей здо- бувача вищої освіти; - enrollTo — відношення, яке вказує на множину навчальних дисциплін (курсів), на які зареєстрований здо- бувач вищої освіти. Створимо конкретний iнстанс сиг- натури Student, що успадковує всi заданi вище вiдношення, а також через оператора fact визначимо початковий набiр базових навичок, інваріантів, які завжди мають бути істинними в усіх допустимих випадках мо- делі. Нижче наведено фрагмент такого фо- рмалiзму: one sig Alice extends Student {}, fact CareerAssignments { Alice.acquiredSkills = A2 + Microsoft_Access Alice.aspiresTo = Business_Analyst } Як уже згадувалося, сутність Student через відношення enrollTo пов'язана з сут- ністю Subject. Створення такого типу від- ношення дозволить нам проаналізувати до- сяжність побудованих траєкторій згідно із 91 Інформатизація науки і освіти заданими обмеженнями та початковими iн- варiантами, заданими вище. Розглянемо си- гнатуру(сутнicть) типу Subject та його набiр вiдношень: abstract sig Subject { provide: set Skill, requires: set Skill } Фактично ми маємо два вiдношення provide та requires із множиною навичок: - provide - вiдношення, що визначає множину навичок, яка дана дисцип- ліна надає після прослуховування; - requires - відношення, що визначає множину навичок, необхiдних як ба- зовi для успішного засвоєння мате- ріалу курсу. Варто зазначити, що де- які дисципліни можуть мати зна- чення none для цього поля, якщо така дисципліна не потребує спе- цифiчних попередньо засвоєних на- вичок. Створення конкретних iнстансiв типу Skill є аналогічним до інстансів типу Student, тому приклад даного формалiзму не наводимо. Розглянемо фрагмент інваріа- нту SubjectProvide, що описує формальний зв’язок між навчальними дисциплінами (Subject) та навичками (Skill): fact SubjectProvide { English.requires = A2 English.provide = B1 BusinessProcessModeling.requires = none BusinessProcessModeling.provide = Business_Process_Modeling SQLFundamentals.requires = Microsoft_Access SQLFundamentals.provide = SQL_Knowledge …. } Фактично ми вказуємо, що базовий курс “English” надає рівень B1, але потре- бує початкових навичок рівня A2. Аналогі- чно дисципліна “Основи SQL” передбачає опанування навичкою Microsoft Access. Во- дночас дисципліна “Моделювання бізнес- процесів” надає навичку Business_Process_Modeling, але не вимагає попередніх знань. Аналогічною є сигнатура careerAspir, пов'язана зі Student через вiдно- шення aspiresTo, а також інваріант, який визначає необхiдні навички, актуальні на ринку праці. abstract sig careerAspir { necessary: set Skill } fact CareerAssignmentsNecessaty { Business_Analyst.necessary = B1 + Business_Process_Modeling + SQL_Knowledge + ArchiMate_Language … } Обмеження та перевірка досяжності. Обмеження в Alloy використову- ються для формальної перевірки інваріан- тів, тобто властивостей, які мають викону- ватись у будь-якому валідному стані мо- делі. Для побудови коректних персоналізо- ваних траєкторій треба визначити, що ко- жен здобувач вищої освіти повинен мати конкретно сформульовану кар'єрну мету. Цей факт можна визначити наступним чи- ном: assert EachStudentHasCareerAspir { all b: Student \| some b.aspiresTo } Застосування обмеження EachStudentHasCareerAspir дозволяє Alloy Evaluator [17] знайти множину контрпри- кладів (якщо це досяжно). У цьому випадку контрприкладом може бути ситуація, коли буде знайдено хоча б один здобувач вищої освіти, для якого не встановлено кар'єрні цілі. Аналогічно, не менш важливою для валідації є перевірка відсутності дисциплін, які не забезпечують хоча б однієї навички. Цей формалiзм можна виразити наступним чином: assert EachSubjectHasSkill { all s: Subject \| some s.provide } Перевірка відсутності контрприкла- дів лише частково свідчить про коректність побудованої мети. Важливо також переві- рити, чи дійсно виконується умова: ∃s ∈ Student s.aspiresTo.necessary ⊆ s.enrollTo.provide (1) 92 Інформатизація науки і освіти Виразити це в синтаксисі Alloy мо- жна наступним чином: some { std:Student\| std.aspiresTo.necessary in std.enrollTo.provide } (2) Якщо ми хочемо окремо перегля- нути список набутих навичок для певного здобувача освіти або список необхідних на- вичок для визначеної кар'єрної мети, мо- жемо застосувати відповідні команди в Alloy Evaluator: - Alice.aspiresTo.necessary - Alice.enrollTo.provide Результат роботи представлений на рис. 1. Рис. 1. Alloy Evaluator. Список набутих і необхідних навичок відповідно до професій- них уподобань здобувача вищої освіти Як видно з Рис. 1, список навичок є еквівалентним, що загалом свідчить про ко- ректність роботи моделі та відсутність по- рушень. Перевіримо умову (1), яка буде дійсно свідчити, про те що існує хоча б один здобувач вищої освіти, який має пот- рібний набір навичок. На Рис. 2 представ- лено вiдображення цього факту. Рис. 2. Перевірка досяжності професійної мети здобувачем вищої освіти відповідно до алгоритму рекомендації курсів засобами Alloy У цьому випадку ми бачимо, що справді існує один здобувач вищої освіти, який досяг необхідної кількості навичок, що свідчить про досяжність кар'єрної мети та правильність побудови персоналізованої освітньої траєкторії. Наступним нашим кроком є демонс- трація працездатності та правильності по- будованого підходу відповідно до запропо- нованого алгоритму рекомендацій в роботi [18]. У Таблиці 1 представлено початкові навички та набуті після навчання на запро- понованих алгоритмом курсів в синтаксисі мови Notation 3 [11]. 93 Інформатизація науки і освіти Таблиця 1. Навички здобувача вищої освіти до та пiсля застосування алгоритму рекомендації До застосування алгоритму ре- комендації Пiсля застосування алгоритму рекомендації ex:Alice a ex:Student ; ex:acquiredSkills ex:A2, ex:Business_Process_Modeling, ex:Microsoft_Access, ex:Python_Language ; ex:careerAspir ex:Business_Analyst, ex:Software_Architect . ex:Alice a ex:Student ; ex:careerAspir ex:Business_Analyst; ex:acquiredSkills ex:A2, ex:ArchiMate_Language, ex:B1, ex:B2, ex:Business_Process_Modeling, ex:Communication_Advanced_English_Sk ills, ex:Communication_English_Skills, ex:Data_Modeling, ex:ETL_Processes, ex:Microsoft_Access, ex:PowerBI, ex:Python_For_Data, ex:Python_Language, ex:Requirement_Engineering, ex:SQL_Knowledge, ex:UML_Modeling ; Варто зазначити, що наша модель стає з n-iтерацiями. Прикладом таких iтера- цiй може бути пocлiдoвнicть запису на курс {English -> Advanced_English}, фактично нам треба acquiredSkills оновлювати ди- намiчно, але рекурсiя в Alloy має серйозні обмеження [19], тому введемо оновлення в код - стан для моделювання динамiки. sig Student { acquired: State -> set Skill, aspiresTo: set careerAspir, enrollTo: set Subject } Застосувавши розроблену модель специфікації до даного набору початкових навичок та відповідного списку дисциплін отримаємо набір навичок у розрізі кожного стану. Приклад роботи зображено на Рис.3. Як бачимо, в State0 (початковий стан) екві- валентний з RDF-моделлю до застосування алгоритму. Рис. 3. Набуті навички здобувача освіти до станів (1-2) 94 Інформатизація науки і освіти Для перевірки досяжності набору навичок у кінцевому стані треба модифіку- вати умови (2) відповідно до нашого онов- лення. Тому для перевірки вимоги, чи існує хоча б один здобувач освіти, який досяг ка- р'єрної мети, використано оновлену ви- могу: some {s:Student\| s.aspiresTo.necessary in s.acquiredSkill[last] } (3) Перевіряємо умови (3) за допомогою Alloy Evaluator. Результат роботи представ- лено на Рис. 4. Рис. 4. Перевірка досяжності кар’єрної мети здобувача освіти Якщо уважно переглянути результат роботи на Рис. 4, то можна побачити екві- валентний набір навичок у стані last=3 та в Таблиці №1 з RDF-моделлю після застосу- вання алгоритму рекомендації. Даний факт демонструє правильність роботи алгори- тму, представленого в роботі. Висновки У процесі дослідження було проана- лізовано теоретичні засади та практичні підходи до перевірки коректності персона- лізованих освітніх траєкторій у межах су- часної освітньої інженерії. З’ясовано, що персоналізоване навчання як інноваційна педагогічна парадигма потребує не лише розроблення індивідуального маршруту здобувача освіти, а й впровадження механі- змів його верифікації, які забезпечують пе- дагогічну доцільність, адаптивність і відпо- відність реальним цілям та потребам здобу- вача освіти. Аналіз наукових джерел і прикладів застосування цифрових технологій дав змогу виокремити сучасні напрями у вери- фікації персоналізованих траєкторій. Розг- лянуто застосування алгоритмічних підхо- дів, зокрема генетичних алгоритмів і ней- ронних мереж, які дають змогу формувати та перевіряти навчальні маршрути з ураху- ванням освітніх досягнень, мотивації та ін- дивідуального прогресу здобувача. Дослі- джено використання семантичного аналізу мотиваційних і професійних даних, що забезпечує глибше розуміння мотиваційно- ціннісної сфери учня та підвищує валід- ність індивідуального навчального плану. Під час нашого дослідження було розроблено формальну модель алгоритму побудови персоналізованих освітніх траєк- торій засобами мови специфікації Alloy. В 95 Інформатизація науки і освіти результаті роботи було доведено корект- ність і досяжність розробленого алгоритму. У подальших дослідженнях плану- ється розширити список обмежень та пере- вірити правильність побудови персоналізо- ваних освітніх траєкторій відповідно до цих обмежень, а також перевірити траєкто- рії за відсутності недетермінованої поведі- нки. Література 1. Peng H., Spector J. Personalized adaptive learning: an emerging pedagogical approach enabled by a smart learning environment. Smart Learning Environments. 2019. Vol. 6. URL: https://doi.org/10.1186/s40561-019-0089-y 2. Tetzlaff L., Schmiedek F., Brod G. Developing personalized education: a dynamic framework. Educational Psychology Review. 2020. Vol. 33. С. 863–882. URL: https://doi.org/10.1007/s10648-020-09570-w 3. Shemshack A., Spector J. A comprehensive analysis of personalized learning components. Journal of Computers in Education. 2021. Vol. 8. С. 485–503. URL: https://doi.org/10.1007/s40692-021-00188-7 4. Алєксєєва С. Дидактичний алгоритм розроб- лення індивідуальної освітньої траєкторії. Ви- токи педагогічної майстерності. 2023. Вип. 32. С. 5–9. DOI: https://doi.org/10.33989/2075- 146x.2023.32.292607 5. Лавренова М., Лалак Н., Молнар Т., Фенчак Л. Траєкторія розвитку здобувача початкової освіти: від теорії до практики. Вісник Львівсь- кого університету. Серія педагогічна. 2021. Вип. 35. С. 130–138. ISSN 2078-5526. URL: http://publications.lnu.edu.ua/bulletins/index.php /pedagogics/article/view/11314 6. Spivakovsky A., Petukhova L., Anisimova O., Horlova A., Kotkova V., Volianiuk A. ICT as a Key Instrument for a Balanced System of Pedagogical Education. ICTERI. 2020. URL: https://www.scopus.com/record/display. uri?eid=2-s2.0- 85096419582&origin=AuthorNamesList&txGi d=cff8324efb62ed78a72d9cda35befe10 7. Papamitsiou Z. Development and research of algorithms for the formation the individual educational trajectories of students in the digital educational platform. 2019. URL: https://www.semanticscholar.org/paper/Develop ment-and-Research-of-Algorithms-for-the-the- Papamitsiou/be314ade46c3232508961eebf2b6e6 92527fa508 8. Kovaliuk T., Kobets N., Dvornyk V. Information technology for constructing individual educational trajectories based on latent-semantic analysis of motivational letters and professional achievements of students. 2020. С. 115–128. URL: https://www.semanticscholar.org/paper/Informatio n-Technology-for-Constructing-Individual- Kovaliuk- Kobets/89c1e0bb06dcea223278d1f07fbec89a822 917b7 9. W3C Semantic Web Wiki. URL: https://www.w3.org/2001/sw/wiki/Main_Page 10.RDF 1.1 Primer [Електронний ресурс]. W3C. 2014. URL: https://www.w3.org/RDF/ 11.Notation3 (N3): A readable RDF syntax. URL: https://notation3.org/ 12.Berners-Lee T. N3Logic: A logical framework for the World Wide Web. W3C. 2008. URL: https://www.w3.org/DesignIssues/N3Logic 13.Poltoratskyi M., Konnova O. Use of semantic web technologies for validation of educational models. Information Technologies and Learning Tools. 2025. Вип. 106(2). С. 94–106. URL: https://doi.org/10.33407/itlt.v106i2.5985 14.Shapes Constraint Language (SHACL) W3C Recommendation. 20 July 2017. URL: https://www.w3.org/TR/shacl/ 15.SPARQL 1.1 Query Language. W3C Recommendation. 21 March 2013. URL: https://www.w3.org/TR/sparql11-query/ 16.Alloy: A language and analyzer for software modeling URL: https://alloytools.org/ 17.Alloy Analyzer – User Guide. URL: https://alloy.readthedocs.io/en/latest/tooling/an alyzer.html 18.Полторацький М. Один з підходів до ство- рення персоналізованого освітнього середо- вищa. Measuring and computing devices in technological processes, 2026. Вип. 1, с. 77– 86. https://doi.org/10.31891/2219-9365-2026- 85-10 19.Alloy Documentation. Analyzer. URL: https://alloy.readthedocs.io/en/latest/tooling/an alyzer.html References 1. H. Peng, J. Spector, Personalized adaptive learning: an emerging pedagogical approach enabled by a smart learning environment, in: Smart Learning Environments, 2019. doi: 10.1186/s40561-019-0089-y. 2. L. Tetzlaff, F. Schmiedek, G. Brod, Developing personalized education: a dynamic framework, in: Educational Psychology Review, 33 (2020) 863–882. doi: 10.1007/s10648-020-09570-w. 3. A. Shemshack, J. Spector, A comprehensive analysis of personalized learning components, 96 Інформатизація науки і освіти in: Journal of Computers in Education, 8 (2021) 485–503. doi: 10.1007/s40692-021- 00188-7. 4. S. Alekseeva, Didactic algorithm for designing an individual educational trajectory, in: Origins of Pedagogical Mastery, 32 (2023) 5– 9. doi: 10.33989/2075-146x.2023.32.292607. [in Ukrainian] 5. M. Lavrenova, N. Lalak, T. Molnar, L. Fenchak, Development trajectory of primary education students: from theory to practice, in: Visnyk of Lviv University. Pedagogical Series, 35 (2021) 130–138. URL: http://publications.lnu.edu.ua/bulletins/index. php/pedagogics/article/view/11314 6. A. Spivakovsky, L. Petukhova, O. Anisimova, A. Horlova, V. Kotkova, A. Volianiuk, ICT as a key instrument for a balanced system of pedagogical education, in: ICTERI, 2020. URL: https://www.scopus.com/record/display.uri?eid =2-s2.0- 85096419582&origin=AuthorNamesList&txGi d=cff8324efb62ed78a72d9cda35befe10 7. Z. Papamitsiou, Development and research of algorithms for the formation of individual educational trajectories of students in the digital educational platform, 2019. URL: https://www.semanticscholar.org/paper/Develop ment-and-Research-of-Algorithms-for-the-the- Papamitsiou/be314ade46c3232508961eebf2b6e 692527fa508 8. T. Kovaliuk, N. Kobets, V. Dvornyk, Information technology for constructing individual educational trajectories based on latent-semantic analysis of motivational letters and professional achievements of students, 2020, pp. 115–128. URL: https://www.semanticscholar.org/paper/Infor mation-Technology-for-Constructing- Individual-Kovaliuk- Kobets/89c1e0bb06dcea223278d1f07fbec89a 822917b7 9. W3C Semantic Web Wiki, 2001. URL: https://www.w3.org/2001/sw/wiki/Main_Page 10. RDF 1.1 Primer [Electronic resource], W3C, 2014. URL: https://www.w3.org/RDF/ 11. Notation3 (N3): A readable RDF syntax, URL: https://notation3.org/ 12. T. Berners-Lee, N3Logic: A logical framework for the World Wide Web, W3C, 2008. URL: https://www.w3.org/DesignIssues/N3Logic 13. M. Poltoratskyi, O. Konnova, Use of semantic web technologies for validation of educational models, in: Information Technologies and Learning Tools, 106(2) (2025) 94–106. doi: 10.33407/itlt.v106i2.5985. 14. Shapes Constraint Language (SHACL) W3C Recommendation, 2017. URL: https://www.w3.org/TR/shacl/ 15. SPARQL 1.1 Query Language. W3C Recommendation, 2013. URL: https://www.w3.org/TR/sparql11-query/ 16. Alloy: A language and analyzer for software modeling, URL: https://alloytools.org/ 17. Alloy Analyzer – User Guide, URL: https://alloy.readthedocs.io/en/latest/tooling/a nalyzer.html 18. M. Poltoratskyi, One approach to creating a personalized educational environment, in: Measuring and Computing Devices in Technological Processes, 1 (2026) 77–86. doi: 10.31891/2219-9365-2026-85-10. 19. Alloy Documentation. Analyzer. URL: https://alloy.readthedocs.io/en/latest/tooling/a nalyzer.html Дата першого надходження до видання: 30.03.2026 Внутрішня рецензія отримана: 19.04.2026 Зовнішня рецензія отримана: 25.04.2026 Дата прийняття статті до друку: 05.06.2026 Дата публікації: 29.06.2026 Про авторів: Полторацький Максим Юрійович, доктор філософії (інформаційні технології), доцент Poltoratskyi Maxym, Ph.D. (information technology), associate professor https://orcid.org/0000-0001-9861-4438 Волянюк Анастасія Сергіївна, викладачка кафедри педагогіки та психології дошкільної та початкової освіти Volianiuk Anastasiya, instructor, department of pedagogy and psy- chology https://orcid.org/0000-0002-2890-4787 Місце роботи авторів: Херсонський державний університет, Kherson State University тел. +380963102636, E-mail:mpoltoratskyi@ksu.ks.ua avolianiuk@ksu.ks.ua
id	pp_isofts_kiev_ua-article-1029
institution	Problems in programming
keywords_txt_mv	keywords
language	Ukrainian
last_indexed	2026-06-30T01:00:10Z
publishDate	2026
publisher	PROBLEMS IN PROGRAMMING
record_format	ojs
resource_txt_mv	ppisoftskievua/ed/f50fd0fd4faed970ff73c37623e23aed.pdf
spelling	pp_isofts_kiev_ua-article-10292026-06-29T10:43:50Z Formal model for verification of personalized educational trajectories based on ALLOY Формальна модель верифікації персоналізованих освітніх траєкторій на основі ALLOY Poltoratskyi, M.Yu. Volianiuk, A.S. personalized learning; educational trajectory; verification; educational engineering; adaptability; skills; career goal; algorithm; model; course UDC 004.942:37.018.43 персоналізоване навчання; освітня траєкторія; верифікація; освітня інженерія; адаптивність; навички; кар'єрна мета; алгоритм; модель; навчальний курс УДК 004.942:37.018.43 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.Prombles in programming 2026; 2: 87-96 У статті розглянуто проблему верифікації персоналізованих освітніх траєкторій у сучасній освітній інженерії в умовах цифровізації освітнього процесу. Обґрунтовано необхідність перевірки коректності навчальних маршрутів, сформованих з урахуванням індивідуальних освітніх потреб, попереднього досвіду, рівня підготовки та професійних цілей здобувачів освіти. Акцентовано увагу на тому, що ефе ктивність персоналізованого навчання визначається не лише якістю проєктування індивідуальної тра єкторії, а й можливістю її формальної перевірки на узгодженість, повноту та досяжність результатів. Запропоновано формальну модель, реалізовану засобами мови специфікації Alloy, яка дозволяє пере віряти відповідність набутих навичок вимогам кар'єрної мети. У межах моделі визначено ключові сут ності, зокрема здобувача освіти, навчальні дисципліни, набуті та необхідні навички, а також профе сійні орієнтації, і формалізовано зв’язки між ними. Запроваджено систему інваріантів і обмежень, що забезпечують перевірку коректності освітніх траєкторій, включаючи наявність визначеної кар’єрної мети, змістовність навчальних компонентів і відповідність результатів навчання вимогам професійної діяльності. Модель забезпечує динамічну перевірку досяжності освітніх результатів шляхом аналізу змін у наборі набутих навичок на різних етапах навчання. Це дає змогу виявляти потенційні помилки у формуванні траєкторій, оцінювати ефективність алгоритмів рекомендації навчальних дисциплін і підтверджувати досяжність визначених цілей. Отримані результати засвідчують, що застосування фо рмального підходу сприяє підвищенню валідності персоналізованого навчання, обґрунтованості осві тніх рішень та ефективності адаптивних освітніх систем. Перспективи подальших досліджень пов’язані з розширенням системи обмежень, урахуванням невизначеності даних і вдосконаленням ме ханізмів адаптації освітніх траєкторій.Prombles in programming 2026; 2: 87-96 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2026-06-29 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/1029 PROBLEMS IN PROGRAMMING; No 2 (2026); 87-96 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2026); 87-96 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2026); 87-96 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/1029/1097 Copyright (c) 2026 PROBLEMS IN PROGRAMMING
spellingShingle	personalized learning educational trajectory verification educational engineering adaptability skills career goal algorithm model course UDC 004.942:37.018.43 Poltoratskyi, M.Yu. Volianiuk, A.S. Formal model for verification of personalized educational trajectories based on ALLOY
title	Formal model for verification of personalized educational trajectories based on ALLOY
title_alt	Формальна модель верифікації персоналізованих освітніх траєкторій на основі ALLOY
title_full	Formal model for verification of personalized educational trajectories based on ALLOY
title_fullStr	Formal model for verification of personalized educational trajectories based on ALLOY
title_full_unstemmed	Formal model for verification of personalized educational trajectories based on ALLOY
title_short	Formal model for verification of personalized educational trajectories based on ALLOY
title_sort	formal model for verification of personalized educational trajectories based on alloy
topic	personalized learning educational trajectory verification educational engineering adaptability skills career goal algorithm model course UDC 004.942:37.018.43
topic_facet	personalized learning educational trajectory verification educational engineering adaptability skills career goal algorithm model course UDC 004.942:37.018.43 персоналізоване навчання освітня траєкторія верифікація освітня інженерія адаптивність навички кар'єрна мета алгоритм модель навчальний курс УДК 004.942:37.018.43
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/1029
work_keys_str_mv	AT poltoratskyimyu formalmodelforverificationofpersonalizededucationaltrajectoriesbasedonalloy AT volianiukas formalmodelforverificationofpersonalizededucationaltrajectoriesbasedonalloy AT poltoratskyimyu formalʹnamodelʹverifíkacíípersonalízovanihosvítníhtraêktoríjnaosnovíalloy AT volianiukas formalʹnamodelʹverifíkacíípersonalízovanihosvítníhtraêktoríjnaosnovíalloy

Formal model for verification of personalized educational trajectories based on ALLOY

Репозитарії

Схожі ресурси