Пошук академічних текстів

Реєстраційний номер

0216U003108, 0113U000071 , Науково-дослідна робота

Назва роботи

Розробити алгоритми верифікації структурованих систем з мобільними агентами.

Керівник роботи

Летичевський Олександр Адольфович,

Дата реєстрації

14-01-2016

Організація виконавець

Інститут кібернетики ім. В.М.Глушкова НАН України

Опис

1. На основі інсерційних моделей для специфікацій багаторівневих протоколів і програм розроблена система IMS, орієнтована на верифікацію прикладних транзиційних систем. Ця система поєднує в собі фундаментальні розробки з аналізу програм з вимогами реальної інженерної практики проектування. LiveUCM, вхідна мову системи IMS, розроблена на базі широко розповсюдженої і прийнятої в якості міжнародного стандарту графічної мови UCM, в якій в рамках проекту були конкретизовані атомарні дії, так звані зобов'язання . В якості таких було запропоновано використовувати локальні описи - базове поняття в інсерцийних моделях. Це дозволило застосувати комплекс символьного моделювання до аналізу систем, специфікованих на мові LiveUCM. В системі IMS комплексно вирішені задачи символьного перетворення формул логіки, що представляють класи станів прикладної системи, оптимізованої перевірки їх здійсненності. Також запропоновані рішення для задачи перевірки досяжності в просторі таких формул, що включає в себе розробку структури простору символьних станів, реалізацію оптимальних стратегій пошуку в ньому, алгоритми абстракції символьних станів, що забезпечують напівразрешімість процедур. З метою спрощення алгоритмів доведення виконуваності формул при верифікації систем досліджено моделі багатокомпонентних систем, у яких використовуються лише переліковні типи даних. У середовищі системи IMS розроблено та реалізовано базу знань про переходи системи з атрибутами переліковних типів. Головні прикладні області та напрямки, на які орієнтовано та у яких успішно використовуються запропоновані методи та програмний інструментарій - телекомунікація, телематика та підготовка кваліфікованих фахівців у галузі програмування. Прогнозні пропозиції щодо розвитку об'єкта - розширення методології та інструментарію від верифікації програм до їх тестування.

Опис продукції

Розроблено та реалізовано прототип системи для аналізу специфікацій та вимог на розробку прикладних транзиційних систем. Ця система пооб'єднує в собі ідеї зручної для інженерів-проектувальників графічної мови UCM з фундаментальними розробками по аналізу програм, зокрема алгоритми символьного моделювання транзиційних систем, структурування простору символьних станів та розробку оптимальних пошукових стратегій в ньому, процедури абстракції символьних станів.

Автори роботи

Волков Владислав Анатолійович
Годлевський Олександр Богуславович
Гребнєв Валерій Олександрович
Губа Антон Андрійович
Довбиш Валентина Яківна
Колчин Олександр Валентинович
Летичевський Олександр Адольфович
Летичевський Олександр Олександрович
Ляскало Леся Євгеніївна
Матвєєва Людмила Євгенівна