Головна Головна -> Реферати українською -> Дисертації та автореферати -> ВЕРИФІКАЦІЯ ТА ТЕСТУВАННЯ ІНТЕРАКТИВНИХ СИСТЕМ, СПЕЦИФІКОВАНИХ ЗА ДОПОМОГОЮ БАЗОВИХ ПРОТОКОЛІВ

ВЕРИФІКАЦІЯ ТА ТЕСТУВАННЯ ІНТЕРАКТИВНИХ СИСТЕМ, СПЕЦИФІКОВАНИХ ЗА ДОПОМОГОЮ БАЗОВИХ ПРОТОКОЛІВ

Назва:
ВЕРИФІКАЦІЯ ТА ТЕСТУВАННЯ ІНТЕРАКТИВНИХ СИСТЕМ, СПЕЦИФІКОВАНИХ ЗА ДОПОМОГОЮ БАЗОВИХ ПРОТОКОЛІВ
Тип:
Реферат
Мова:
Українська
Розмiр:
15,18 KB
Завантажень:
353
Оцінка:
 
поточна оцінка 5.0


Скачати цю роботу безкоштовно
Пролистати роботу: 1  2  3  4  5  6  7  8  9 
Національна академія наук України
Інститут кібернетики імені В.М. Глушкова
ЛЕТИЧЕВСЬКИЙ Олександр Олександрович
УДК 681.3.06
ВЕРИФІКАЦІЯ ТА ТЕСТУВАННЯ ІНТЕРАКТИВНИХ СИСТЕМ, СПЕЦИФІКОВАНИХ ЗА ДОПОМОГОЮ БАЗОВИХ ПРОТОКОЛІВ
01.05.03 – математичне та програмне забезпечення обчислювальних машин і систем
Автореферат
дисертації на здобуття наукового ступеня
кандидата фізико-математичних наук
Київ – 2005


Дисертацією є рукопис.
Робота виконана в Інституті кібернетики ім. В.М. Глушкова НАН України.
Науковий керівник: доктор фізико-математичних наук, професор
Капітонова Юлія Володимирівна,
Інститут кібернетики ім. В.М.Глушкова НАН України,
завідуюча відділом
Офіційні опоненти: доктор фізико-математичних наук, професор
Асельдеров Зайнутдін Макашаріпович,
Національний технічний університет України ”КПІ”,
.
кандидат фізико-математичних наук
Бублик Володимир Васильович,
Київський національний університет імені Тараса Шевченка
Провідна установа: Інститут програмних систем НАН України, відділ теорії комп’ютерних обчислень
Захист відбудеться “___” _______________2005 р. о (об) _______ годині на засіданні
спеціалізованої вченої ради Д 26.194.02 при Інституті кібернетики ім. В.М.Глушкова НАН України за адресою:
03680, МСП, Київ-187, проспект Академіка Глушкова, 40.
З дисертацією можна ознайомитися в науково-технічному архіві Інституту кібернетики ім. В.М. Глушкова НАН України.
Автореферат розісланий “___” __ 2005 р.
Учений секретар
спеціалізованої вченої ради Синявський В.Ф.
ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ
Актуальність теми. Верифікація і тестування систем є найважливішими задачами, вирішення яких визначає якість програмного забезпечення. Сучасні індустріальні програмні системи, що використовуються, зокрема в галузі телекомунікацій, нараховують десятки тисяч вимог. Тому при їх створенні імовірність появи помилок досить висока. Використання методів верифікації вимог для виявлення помилок уже на етапі збору вимог дозволить зменшити кількість помилок, які визначаються на етапі кодування, і відповідно скоротити час розробки систем та підвищити їх якість. З іншого боку, створення набору символьних тестів, що покриває усі вимоги, є найважливішою задачею тестування індустріальних систем.
У сучасній літературі існує клас методів, призначений для автоматичного аналізу формальних специфікацій і генерації з них тестів. Методи цього класу розбиваються на дві частини. Перша частина належить до так званого Model Checkіng – перевірки моделі, заданої формальними специфікаціями, а друга – пов’язана з доказом тверджень, що характеризують поводження системи, наприклад, її критичних властивостей – lіveness (життєздатність), safety (цілісність) і т.п. Model Checkіng, в основному, застосовується до формальної верифікації систем з скінченним числом станів. Формалізовані вимоги виражені формулами темпоральної логіки, а ефективні символьні алгоритми використовуються для обробки моделі і перевірки, чи відповідають вони вимогам, чи ні. Для перевірки систем з великою кількістю станів використовуються системи Verіsoft, SMV, SPІ, SCR, Murphі. Основною проблемою даного підходу є проблема експоненційного вибуху множини досліджуваних станів .
До систем, що працюють з доказами тверджень, належить система HOL, яка є середовищем для інтерактивного доказу теорем у логіці вищих порядків. Система PVS також працює з логіками вищих порядків і абстрактних типів даних.
Використання цих методів було успішно впроваджене стосовно специфікацій, виражених мовами MSC, SDL, UML, які всіляко застосовуються в інженерних розробках. Фірми Telelogіc і іLogіc брали участь у проекті OMEGA, що призначався з метою розробки формальних засобів для застосування на різних стадіях дизайну UML-специфікацій. У корпорації Sіemens була проведена верифікація частини GSM-протоколу з використанням засобів SVE. Інтегрована система для обробки SDL-специфікацій була реалізована на базі доказової машини ACL2.
Мова MSC також є одним з об'єктів застосування формальних методів.

Завантажити цю роботу безкоштовно
Пролистати роботу: 1  2  3  4  5  6  7  8  9 



Реферат на тему: ВЕРИФІКАЦІЯ ТА ТЕСТУВАННЯ ІНТЕРАКТИВНИХ СИСТЕМ, СПЕЦИФІКОВАНИХ ЗА ДОПОМОГОЮ БАЗОВИХ ПРОТОКОЛІВ

BR.com.ua © 1999-2017 | Реклама на сайті | Умови використання | Зворотній зв'язок