Дорогий, Я. Ю.Цуркан, В. В.Dorogyy, Yaroslaw Yu.Tsurkan, Vasyl V.2021-04-072021-04-0720202311–3405 (Print)2313-0415 (Online)https://eir.nuos.edu.ua/handle/123456789/3802Дорогий, Я. Ю. Огляд методів верифікації параметризованих моделей = A survey of parametric model verification methods / Я. Ю. Дорогий, В. В. Цуркан // Зб. наук. пр. НУК. – Миколаїв : НУК, 2020. – № 1 (479). – С. 82–90.Анотація. Фактично сьогодні відсутній сучасний огляд методів верифікації параметризованих моделей, який би чітко відповів на питання щодо доцільності використання того чи іншого підходу до верифікації параметризованих моделей. Саме тому метою дослідження є аналіз методів верифікації параметризованих моделей. Під час проведення дослідження застосовувалися методи системного аналізу, порівняння та аналізу. Проведено аналіз методів верифікації параметризованих моделей, серед яких досліджено чотири групи методів, таких як аналітичні методи редукції, методи абстракції, символьні методи та методи, засновані на пошуку інваріантів. В аналітичних методах редукції, як правило, зазначається спосіб відображення моделей сімейства параметризованих моделей на одну модель цього сімейства. Для методів абстракції також часто зазначається спосіб відображення параметризованих моделей на одну модель, але ця модель не належить самому параметризованому сімейству, а моделює поведінку будь-якого числа однотипних процесів. Зі способу відображення випливають структурні обмеження на параметризовані сімейства моделей, які можуть бути верифіковані в такий спосіб. Символьні методи зазвичай використовують модифікації символьного підходу до розв’язання задачі верифікації моделей. У методах, заснованих на пошуку інваріанта, шукається або конструюється процес-інваріант, що моделює поведінку декількох процесів системи. В ході дослідження визначено їх основні характеристики, недоліки та переваги. Символьні методи застосовуються переважно для перевірки властивостей безпеки, тоді як багато методів інваріантів застосовні також для перевірки властивостей живучості. Для застосування символьних методів опис параметризованої моделі потрібно представити спеціальною мовою методу, яка зазвичай досить сильно відрізняється від мов опису моделей засобів верифікації моделей. Методи інваріантів використовують описи процесів у вигляді транзиційних систем, розмічених пропозиціональними змінними, а також сумісні з мовами опису моделей засобів верифікації моделей. Методи інваріантів використовують для перевірки специфікації та пошуку контрприкладів наявні засоби верифікації моделей, символьні ж методи вимагають реалізації спеціальних алгоритмів. Як наслідок, визначено найкращу групу методів, яка не потребує розроблення нових мов опису та спеціальних алгоритмів.ukпараметризована модельметод абстракціїметод пошуку інваріантівтранзиційна системарозмічена транзиційна системаконтекстно-вільна граматикаparameterized modelabstraction methodinvariant search methodtransition systemlabeled transition systemcontext-free grammarArticle