Алгебраїчні методи верифікації асинхронних паралельних систем - Автореферат

Національна академія наук України Інститут кібернетики імені В.М. Глушкова УДК 519.686.4 АВТОРЕФЕРАТ дисертації на здобуття наукового ступеня кандидата фізико-математичних наук Алгебраїчні методи верифікації асинхронних паралельних систем 01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем Потієнко Степан Валерійович Київ - 2009 Дисертацією є рукопис. Робота виконана в Інституті кібернетики імені В.М. Глушкова НАН України. Науковий керівник:доктор фізико-математичних наук, професор, академік НАН України Летичевський Олександр Адольфович, Інститут кібернетики імені В.М. Глушкова НАН України, завідуючий відділом. Автореферат розісланий 10.05. 2009 р. Учений секретар спеціалізованої вченої ради Синявський В.Ф. Загальна характеристика роботи Актуальність теми. Застосування методів формального опису вимог є невідємною частиною сучасного процесу розробки складних програмних систем. Існує два загально відомих підходи до верифікації - це перевірка на моделі (model checking) і доведення теорем (theorem proving). Перевірка на моделі - техніка, яка застосовується до моделей із скінченою множиною станів і перевіряє, що задані властивості виконуються на цій моделі. У даній роботі ця проблема вирішується завдяки розробленим алгоритмам трансляції таких розповсюджених стандартизованих мов моделювання, як MSC, SDL та UML, в мову базових протоколів, яка є основним формалізмом у роботі. Робота виконувалась у рамках праць Інституту кібернетики імені В.М. Глушкова НАН України «Розробити методи інтелектуалізації інформаційних технологій для оптимізації паралельних обчислень і верифікації дедуктивними методами паралельних програм, що масштабуються» (шифр ВФК.105.02, номер держкеєстрації 0107U003570); «Розробити та дослідити ефективні методи специфікації та генерації безпечних систем у техногенному середовищі» (шифр В.Ф.100.08, номер держреєстрації 0108U000105); «Розробити теорію та методи інерційного моделювання та верифікації багаторівневих взаємодіючих систем» (шифр В.Ф.105.03, номер держреєстрації 0108U000106), а також у рамках проекту Верифікація вимог до систем виконуваного в компанії Інформаційні програмні системи разом з Інститутом кібернетики імені В.М. Глушкова НАН України і компаніями Motorola, Hengsoft. В роботах, виконаних у співавторстві, С.В. Потієнко вніс такий вклад: у роботі [1] автором розроблено алгоритм нормалізації SDL моделі та трансляції конструкцій start, state, save, input, output, set, reset, timeout в мову базових протоколів; [2] - розроблено алгоритм трансляції керуючих конструкцій MSC alt, opt, exc, loop та par в мову базових протоколів та запропоновано розширення MSC сценаріїв анотаціями; [5] - розроблено алгоритми перевірки транзиційної повноти та несуперечливості базових протоколів, а також алгоритм перевірки коректності анотацій в MSC сценаріях; [6] - розроблено алгоритм анотаційного чекеру SDL специфікацій; [9] - створено опис середовища для верифікації MPI програм, а також синтаксис та семантику інтерпретації процесів у базових протоколах для формалізації функцій бібліотеки MPI.