Закутайло Денис Олександрович. Коректне проектування апаратно-програмних засобiв обчислювальної технiки на основi логiчних мов специфiкацiй i сучасних мов опису дискретних систем

brief description

Закутайло Денис Олександрович. Коректне проектування апаратно-програмних засобiв обчислювальної технiки на основi логiчних мов специфiкацiй i сучасних мов опису дискретних систем : Дис... канд. наук: 05.13.13 - 2007.

Закутайло Д.О. Коректне проектування апаратно-програмних засобів обчи-слювальної техніки на основі логічних мов специфікацій і сучасних мов опису дискретних систем. Рукопис.
Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 05.13.13 обчислювальні машини, системи та мережі. Інститут кібернетики ім. В.М. Глушкова НАН України, Київ, 2006.
Наукова новизна отриманих результатів полягає в наступному: розроблені часові логіки LCTL і GCTL, що дозволяють кількісно характеризувати часові властивості алгоритмів, що верифікуються. Семантика цих часових логік, дозволяє використовувати моделі алгоритмів, що верифікуються, із числом станів меншим, чим у відповідних моделей для існуючих раніше часових логік і їх семантик; уперше запропоновані методи трансляції програм з мови VHDL, що засто-совувають конструкції з часовими затримками, у транзиційні системи; для запро-понованих логік розроблені методи перевірки властивостей з явними часовими обмеженнями, отримана оцінка часової складності запропонованого методу перевірки на моделі для логіки LCTL.
Практичне значення розробленої системи для верифікації цифрових пристроїв, описаних мовою VHDL, полягає в тісній інтеграції із існуючими САПР, обліку явних часових затримок. Запропоновані алгоритми дозволили верифікувати транзиційні системи практичного рівня складності з часовими обмеженнями на переходи.
Реалізація на практиці отриманих результатів дозволяє значно скоротити строки розробок, істотно зменшивши обсяг робіт, пов'язаних із забезпеченням коректності функціонування апаратно-програмних систем.

Сукупність отриманих у дисертації результатів пов'язана з розробкою підходу до верифікації алгоритмів функціонування дискретних систем, що задовольняють заданим часовим обмеженням. На основі методу перевірки властивостей на моделі, що обумовило розробки відповідних часових логік для опису властивостей алгоритмів і методів побудови моделей алгоритмів, описаних у сучасних мовах проектування.
При цьому отримані основні результати дисертаційної роботи такі:
1) одержала подальший розвиток теорія часових логік, а саме: розроблено часові логіки, що дозволяють кількісно характеризувати часові властивості алгоритмів, що верифікуються. Семантика цих часових логік, дозволяє використовувати моделі алгоритмів із числом станів меншим, ніж у відповідних моделях для існуючих часових логік і їх семантик;
2) уперше запропоновано методи трансляції програм з мови VHDL, що застосовує конструкції з часовими затримками, у транзиційні системи. Використання конструкцій мови VHDL з часовими затримками дозволяє істотно скоротити строки розробки дискретних систем;
3) реалізовано новий транслятор з мови VHDL у функції переходів тран-зиційної системи;
4) одержав подальший розвиток метод перевірки на моделі, а саме: для запропонованих логік розроблені методи перевірки властивостей з явними часовими обмеженнями, отримано поліноміальну оцінку часової складності запропонованого методу перевірки на моделі для логіки LCTL;
5) для дослідження властивостей одної із запропонованих часових логік (LCTL) реалізована система для перевірки виконуваності формул цієї логіки;
6) розроблено автоматизовану систему верифікації цифрових систем, описаних мовою VHDL, що використовує запропоновані часові логіки.
Реалізація на практиці вищеперерахованих результатів дозволяє значно скоротити строки розробок, істотно зменшивши обсяг робіт, пов'язаних із забез-печенням коректності функціонування апаратно-програмних систем.