Диссертации и авторефераты Украины
Перейти на каталог
Каталог диссертаций

Я ищу:
Диссертация / Автореферат

Диссертационная работа:

Колчин Олександр Валетнинович. Розробка інструментальних засобів для перевірки формальних моделей асинхронних систем : Дис... канд. наук: 01.05.03 - 2009.

Скачать диссертацию *

* Ссылка размещена на правах рекламы



Аннотация к работе:

Колчин О.В. Розробка інструментальних засобів для перевірки формальних моделей асинхронних систем. – Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 – математичне та програмне забезпечення обчислювальних машин і систем. – Інститут кібернетики імені В.М. Глушкова НАН України, Київ, 2009.

Робота присвячена створенню алгоритмів та методів для автоматичної верифікації формальних моделей великих промислових систем.

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

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

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

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

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

– Проведено порівнювальний аналіз із сучасними методами побудови абстракцій, виділено принципові розрізнення; результати проведених експериментів продемонстрували високу ефективність порівняно з існуючими відомими системами та методами верифікації. Так, перевірка властивостей моделі у наведеному прикладі такими популярними системами верифікації як SMV, NuSMV, VCEGAR, BLAST, SPIN показала експоненційну складність (по часу та кількості станів, а у деяких випадках і по кількості ітерацій уточнень абстракцій). Експеримент з реалізацією описаного методу показав квадратичну залежність від розміру задачі.

– Побудовано метод спрямованого пошуку поведінки моделі, який може бути використаний для опису критеріїв покриття з метою генерації тестових сценаріїв на основі моделі. Запропонований метод є різновидом обмеженої перевірки моделі; як обмежувачі використовує цілі тестування, які визначає користувач. На відміну від існуючих методів спрямування пошуку
й генерації тестів, напрямком для пошуку служить зразок – спеціальний обмежений регулярний вираз над алфавітом імен переходів моделі. Такий зразок є «шаблоном» тестового сценарію, використовується для відсічення несумісних гілок поведінки моделі і водночас для перевірки на припустимість передбаченої поведінки. При цьому, по суті, здійснюється валідація моделі. Включення операції ітерації в опис напрямку дає можливість перевіряти порушення специфічних властивостей, наприклад, наявність нескінченних циклів за відсутності зовнішніх сигналів. Ефективно знаходити важко досяжні стани дозволяє використання коротких дистанцій та заборон між контрольними точками зразків. Техніка послаблення еквівалентності трас і станів суттєво скорочує кількість тестових сценаріїв, які забезпечують необхідне покриття, та час їх пошуку.

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

– Створено програмний комплекс, який реалізує алгоритми побудови абстракцій та спрямованого пошуку. Комплекс впроваджено у промислову розробку – систему VRS і успішно застосовано у 9 промислових проектах.


Меню
Реклама



2006-2009 © Диссертации и авторефераты Украины