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

Наукова новизна отриманих результатiв полягає в наступному: розробленi часовi логiки LCTL (Локальна обчислювальна логiка розгалуженого часу) i GCTL (Глобальна обчислювальна логiка розгалуженого часу), що дозволяють кiлькiсно характеризувати часовi властивостi алгоритмiв, що верифiкуються. Семантика цих часових логiк, дозволяє використовувати моделi алгоритмiв, що верифiкуються, iз числом станiв меншим, чим у вiдповiдних моделей для iснуючих ранiше часових логiк i їх семантик; уперше запропонованi методи трансляцiї програм з мови VHDL, що застосовувають конструкцiї з часовими затримками, у транзицiйнi системи; для запропонованих логiк розробленi методи перевiрки властивостей з явними часовими обмеженнями, отримана оцiнка часової складностi запропонованого методу перевiрки на моделi для логiки LCTL.