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