У дисертаційній роботі розглянуто проблеми побудови точних абстракцій станів моделі, спрямованого пошуку поведінки моделі й генерації тестових сценаріїв на основі моделі, а також проблема автоматизації побудови формальних моделей. Отримано наступні результати: – Побудовано метод оперативної побудови точних абстракцій для перевірки темпоральних властивостей. Метод повністю автоматичний, не потребує втручання з боку користувача, не суперечить методам часткового порядку, методам, які застосовують симетрії, а також може бути використаний сумісно із символьними методами абстракції предикатів, що будують абстракції до виконання перевірки моделі. – Побудовано алгоритм верифікації, що реалізує метод побудови абстракцій станів моделі. Алгоритм завжди видає точні результати та не потребує повторних запусків для уточнень абстракцій. Абстракцією є сюр’єктивне тотальне функціональне відношення, що зберігає реальні значення атрибутів відповідного конкретного стану. Абстрактні стани формуються динамічно у процесі аналізу властивостей моделі, таким чином, на відміну від статичних методів, ігноруються залежності атрибутів, які обумовлені недосяжними переходами. Гарантується точність результатів: доведено, зокрема, що побудована абстракція конкретної АТС щодо властивостей, які перевіряються , завжди задовольняє властивості . При цьому асимптотичний час роботи алгоритму побудови абстракцій не гірший ніж у класичних алгоритмів. – Проведено порівнювальний аналіз із сучасними методами побудови абстракцій, виділено принципові розрізнення; результати проведених експериментів продемонстрували високу ефективність порівняно з існуючими відомими системами та методами верифікації. Так, перевірка властивостей моделі у наведеному прикладі такими популярними системами верифікації як SMV, NuSMV, VCEGAR, BLAST, SPIN показала експоненційну складність (по часу та кількості станів, а у деяких випадках і по кількості ітерацій уточнень абстракцій). Експеримент з реалізацією описаного методу показав квадратичну залежність від розміру задачі. – Побудовано метод спрямованого пошуку поведінки моделі, який може бути використаний для опису критеріїв покриття з метою генерації тестових сценаріїв на основі моделі. Запропонований метод є різновидом обмеженої перевірки моделі; як обмежувачі використовує цілі тестування, які визначає користувач. На відміну від існуючих методів спрямування пошуку
й генерації тестів, напрямком для пошуку служить зразок – спеціальний обмежений регулярний вираз над алфавітом імен переходів моделі. Такий зразок є «шаблоном» тестового сценарію, використовується для відсічення несумісних гілок поведінки моделі і водночас для перевірки на припустимість передбаченої поведінки. При цьому, по суті, здійснюється валідація моделі. Включення операції ітерації в опис напрямку дає можливість перевіряти порушення специфічних властивостей, наприклад, наявність нескінченних циклів за відсутності зовнішніх сигналів. Ефективно знаходити важко досяжні стани дозволяє використання коротких дистанцій та заборон між контрольними точками зразків. Техніка послаблення еквівалентності трас і станів суттєво скорочує кількість тестових сценаріїв, які забезпечують необхідне покриття, та час їх пошуку. – Побудовані транслятори специфікацій табличних і текстових типів у формальну модель. Автоматизована побудова формальної моделі дозволяє уникнути необхідності явного введення допоміжних атрибутів, зберегти компактність і структурованість вихідного опису моделі, що дозволяє суттєво зменшити об’єми та підвищити якість формалізації, а також скоротити трудовитрати та час виконання задач верифікації в цілому. – Створено програмний комплекс, який реалізує алгоритми побудови абстракцій та спрямованого пошуку. Комплекс впроваджено у промислову розробку – систему VRS і успішно застосовано у 9 промислових проектах. |
