Огляд методів верифікації параметризованих моделей
Вантажиться...
Дата
2020
Автори
Дорогий, Я. Ю.
Цуркан, В. В.
Dorogyy, Yaroslaw Yu.
Tsurkan, Vasyl V.
Назва журналу
Номер ISSN
Назва тому
Видавець
Анотація
Анотація. Фактично сьогодні відсутній сучасний огляд методів верифікації параметризованих моделей, який би чітко відповів на питання щодо доцільності використання того чи іншого підходу до верифікації параметризованих моделей. Саме тому метою дослідження є аналіз методів верифікації параметризованих моделей. Під час проведення дослідження застосовувалися методи системного аналізу, порівняння та аналізу. Проведено аналіз методів верифікації параметризованих моделей, серед яких досліджено чотири групи методів, таких як аналітичні методи редукції, методи абстракції, символьні методи та методи, засновані на пошуку інваріантів. В аналітичних методах редукції, як правило, зазначається спосіб відображення моделей сімейства параметризованих моделей на одну модель цього сімейства. Для методів абстракції також часто зазначається спосіб відображення параметризованих моделей на одну модель, але ця модель не належить самому параметризованому сімейству, а моделює поведінку будь-якого числа однотипних процесів. Зі способу відображення випливають структурні обмеження на параметризовані сімейства моделей, які можуть бути верифіковані в такий спосіб. Символьні методи зазвичай використовують модифікації символьного підходу до розв’язання задачі верифікації моделей. У методах, заснованих на пошуку інваріанта, шукається або конструюється процес-інваріант, що моделює поведінку декількох процесів системи. В ході дослідження визначено їх основні характеристики, недоліки та переваги. Символьні методи застосовуються переважно для перевірки властивостей безпеки, тоді як багато методів інваріантів застосовні також для перевірки властивостей живучості. Для застосування символьних методів опис параметризованої моделі потрібно представити спеціальною мовою методу, яка зазвичай досить сильно відрізняється від мов опису моделей засобів верифікації моделей. Методи інваріантів використовують описи процесів у вигляді транзиційних систем, розмічених пропозиціональними змінними, а також сумісні з мовами опису моделей засобів верифікації моделей. Методи інваріантів використовують для перевірки специфікації та пошуку контрприкладів наявні засоби верифікації моделей, символьні ж методи вимагають реалізації спеціальних алгоритмів. Як наслідок, визначено найкращу групу методів, яка не потребує розроблення нових мов опису та спеціальних алгоритмів.
Опис
Дорогий, Я. Ю. Огляд методів верифікації параметризованих моделей = A survey of parametric model verification methods / Я. Ю. Дорогий, В. В. Цуркан // Зб. наук. пр. НУК. – Миколаїв : НУК, 2020. – № 1 (479). – С. 82–90.
Ключові слова
параметризована модель, метод абстракції, метод пошуку інваріантів, транзиційна система, розмічена транзиційна система, контекстно-вільна граматика, parameterized model, abstraction method, invariant search method, transition system, labeled transition system, context-free grammar