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

Помилки у функціонуванні таких систем, як системи керування ядерними реакторами, хімічним виробництвом, засобами космічної техніки можуть призвести до катастрофічних наслідків, повязаних з великими матеріальними втратами й людськими жертвами. Тому до надійності й безпомилковості функціонування таких систем предявляються надзвичайно суворі вимоги, для задоволення яких необхідні методи коректного проектування такого роду систем. Тому при проектуванні високо надійних систем важливого значення набуває використання формальних методів, що засновані на мовах, методах і інструментальних засобах для специфікації й верифікації таких систем. Метою дисертаційної роботи є розробка методів верифікації алгоритмів функціонування дискретних систем, що задовольняють заданим часовим обмеженням, на основі методу перевірки властивостей на моделі, що вимагає розробки відповідних часових логік для опису властивостей алгоритмів і методів побудови моделей систем, описаних у сучасних мовах проектування. Методи досліджень ґрунтуються на теорії автоматів, яку застосовано для розробки лексичного й синтаксичного аналізаторів системи верифікації; теорії графів, яку застосовано для розробки алгоритму перевірки на моделі формул запропонованої логіки LCTL, за допомогою обходу графа переходів пристрою, що верифікується; теорії складності, що дозволяє дати теоретичну оцінку складності розроблених алгоритмів; теорії часових логік, яку застосовано для опису властивостей системи, що верифікуються; теорії нерухомої точки, за допомогою якої описані всі оператори логіки LCTL.Семантика операторів логіки LCTL збігається із семантикою однойменних операторів логіки CTL, для інших операторів логіки LCTL відношення виконуваності формули в стані структури визначається в такий спосіб: 1) коли в кожному шляху, що починається в, у стані цього шляху істинна формула, і час, за який з досягне, задовольняє умові; 3) коли в кожному шляху, що починається в, існує такий стан, що формула істинна в ньому, і у всіх станах цього шляху, де істинні формула й помилкова формула, і сумарний час, за який з досягне, задовольняє умові; 4) коли існує шлях, що починається в, у стані якого істинна формула, і у всіх станах цього шляху, де істинні формула й помилкова формула, і сумарний час, за який з досягне, задовольняє умові; 3) коли в кожному шляху, що починається в, існує такий стан, в якому істинна формула й у всіх станах цього шляху, де істинні формула й заперечення формули, і час, що дорівнює плюс час, за який з досягається, задовольняє умові; 4) коли існує такий шлях, що починається в, і в стані якого істинна формула, і у всіх станах цього шляху, де істинні формула й заперечення формули, і час, що дорівнює плюс час, за який з досягається, задовольняє умові;Сукупність отриманих у дисертації результатів повязана з розробкою підходу до верифікації алгоритмів функціонування дискретних систем, що задовольняють заданим часовим обмеженням, на основі методу перевірки властивостей на моделі, що обумовило розробки відповідних часових логік для опису властивостей алгоритмів і методів побудови моделей алгоритмів, описаних у сучасних мовах проектування. При цьому були отримані наступні основні результати: 1) Одержала подальший розвиток теорія часових логік, а саме: розроблено часові логіки, що дозволяють кількісно характеризувати часові властивості алгоритмів, що верифікуються.

ОСНОВНИЙ ЗМІСТ ДОСЛІДЖЕННЯ

Сукупність отриманих у дисертації результатів повязана з розробкою підходу до верифікації алгоритмів функціонування дискретних систем, що задовольняють заданим часовим обмеженням, на основі методу перевірки властивостей на моделі, що обумовило розробки відповідних часових логік для опису властивостей алгоритмів і методів побудови моделей алгоритмів, описаних у сучасних мовах проектування.

При цьому були отримані наступні основні результати: 1) Одержала подальший розвиток теорія часових логік, а саме: розроблено часові логіки, що дозволяють кількісно характеризувати часові властивості алгоритмів, що верифікуються. Семантика цих часових логік, дозволяє використовувати моделі алгоритмів із числом станів меншим, ніж у відповідних моделях для існуючих часових логік і їх семантик;

2) Уперше запропоновано методи трансляції програм з мови VHDL, що застосовує конструкції з часовими затримками, у транзиційні системи. Використання конструкцій мови VHDL з часовими затримками дозволяє істотно скоротити строки розробки дискретних систем;

3) Реалізовано транслятор з мови VHDL у функції переходів транзиційної системи;

4) Одержав подальший розвиток метод перевірки на моделі, а саме: для запропонованих логік розроблені методи перевірки властивостей з явними часовими обмеженнями, отримано поліноміальну оцінку часової складності запропонованого методу перевірки на моделі для логіки LCTL;

5) Для дослідження властивостей одної із запропонованих часових логік (LCTL) реалізована система для перевірки виконуваності формул цієї логіки;

6) Розроблено автоматизовану систему верифікації цифрових систем, описаних мовою VHDL, що використовує запропоновані часові логіки.

Реалізація на практиці перерахованих вище результатів дозволяє значно скоротити строки розробок, істотно зменшивши обсяг робіт, повязаних із забезпеченням коректності функціонування апаратно-програмних систем.

Можливі напрямки розвитку даної роботи. Необхідно верифікувати значно більше описів електронних пристроїв на VHDL за допомогою розробленої системи верифікації. Аналіз прикладів верифікації конкретних пристроїв дозволить увести ряд необхідних операторів, що спрощують специфікацію властивостей, що верифікуються.

У даній роботі запропоновані методи перетворення найбільш уживаних конструкцій мови VHDL у функції переходів. Бажано розширити кількість перетворюваних конструкцій до повного стандарту мови. Це дозволило б розглядати кінцеву програму як комерційний продукт, а не як дослідницьку роботу.

1. Закутайло Д.А. Использование структур данных типа BDD для формальной верификации аппаратуры // Нові компютерні засоби, обчислювальні машини та мережі. - Киев: Институт кибернетики имени В.М. Глушкова, 2001. - Т.1. - С. 140-152.

2. Закутайло Д.А. Современные автоматизированные системы для формальной верификации аппаратуры (обзор) // Засоби компютерної техніки з віртуальними функціями і нові інформаційні технології. - Киев: Институт кибернетики имени В.М. Глушкова, 2002. - С. 99-104.

3. Закутайло Д.А. Автоматизированная система верификации цифровых систем // Искусственный интеллект. - Донецк: Институт проблем искусственного интеллекта, 2003. - №3. - С. 95-101.

4. Закутайло Д.А. Трансляция VHDL программы в BDD структуры // Компютерні засоби, мережі та системи. - Киев: Институт кибернетики имени В.М. Глушкова, 2003. - №2. - С. 144-150.

5. Закутайло Д.А. Язык спецификации временных свойств дискретных систем // Международная научно-техническая конференция "Искусственный интеллект". - Таганрог, Изд-во ТРТУ: 2002. - Т.1. - С. 236-237.

6. Закутайло Д.А. Автоматизированная система верификации цифровых систем // Международная научно-техническая конференция "Интеллектуальные и многопроцессорные системы-2003". - Таганрог, Изд-во ТРТУ: 2003. - Том 2. - С. 113-116.