Номер роботи - M 96 ДОПУЩЕНА ДО УЧАСТІ
Автори: Песчаненко В.С., к.ф.-м.н., Блинов І.О., Кльонов Д.М.
Представлена Херсонським державним університетом
У роботі розглянуто оптимізацію математичного та програмного забезпечення, яка використовується для доведення властивостей інсерційних моделей.
Надано огляд перевіряємих властивостей, сучасних систем та методів верифікації формальних моделей. Стисло описані основні теоретичні відомості про інсерційне моделювання. Висвітлено алгоритми перевірки здійсненності формул, прямого та зворотного предикатних трансформерів.
Створено алгоритм усунення інтерлівінгу у символьних інсерційних моделях, введені поняття необхідної та достатньої умов перестановочності операторів, у тому числі поняття статичної та динамічної перестановочності. Узагальнено алгоритм для перевірки досяжності деяких станів користувача. Описано алгоритм розділення формули на спеціалізації, абстрактний предикатний трансформер, який є інваріантним відносно структур даних дедуктивної системи. Представлено алгоритм конкретизації символьних трас, який дозволяє отримувати конкретну трасу, що покривається висхідною символьною трасою. Висвітлено алгоритми змішаних обчислень для інсерційних моделей. Доведено існування оберненої поведінки у повній розширеній алгебрі поведінки. Удосконалено мову RЕМ, за допомогою вдосконалення якої доведено ефективність за часом недетермінованої стратегії переписування. Одержано ефективний алгоритм трансляції коду мовою APLAN до мови С++.
Коротко описана система VRS як комерційна система, у якій використано основні результати дослідження. Представлено систему доказового програмування та елементи констрейтного програмування засобами інсерційного моделювання.
Кількість публікацій: 46, в т.ч. 34 статті, 8 тез доповідей, 4 свідоцтва про реєстрацію авторського права на твір.
Версія для друку