Розробка інструментальних засобів для перевірки формальних моделей асинхронних систем - Автореферат

Національна академія наук України Інститут кібернетики імені В.М..05.03 математичне та програмне забезпечення обчислювальних машин і систем Автореферат дисертації на здобуття наукового ступеня кандидата фізико-математичних наук Науковий керівник: доктор фізико-математичних наук, професор, академік НАН України Офіційні опоненти: доктор фізико-математичних наук, професор Захист відбудеться 12.06. 2009 р. о(об) 11 годині на засіданні спеціалізованої вченої ради Д 26.194.02 при Інституті кібернетики імені В.М.Методи тестування не забезпечують вичерпного аналізу усіх можливих варіантів поведінки, тим самим не можуть гарантувати відсутність порушень властивостей, якими мають володіти системи, що розроблюються. Моделі, що перевіряються, представляються у вигляді графа переходів станів, а властивості формулюються у темпоральній логіці. Системи, які дозволяють автоматизувати побудову тестових сценаріїв на етапі верифікації, зазвичай оцінюють повноту покриття тестовим набором за такими метриками та критеріями: кількість виповнених операторів та гілок програми, покриття предикатів моделі і граничних значень функцій, переходів між станами та ін. Однак питання про те, у якому співвідношенні знаходяться такі показники тестового покриття моделі і покриття основних вимог до цільової системи в загальному випадку, як правило, не розглядається, і як наслідок відповідності між отриманими тестовими сценаріями, котрі задовольняють вищеописаним критеріям, та основними функціональними специфікаціями до цільової системи немає. Тому актуально створення методу спрямованого пошуку поведінки моделі, метою якого є генерація тестових сценаріїв, які задовольняють заданим критеріям покриття вимог до системи.Робота присвячена розробці автоматичних методів та алгоритмів для верифікації формальних моделей асинхронних систем та побудови на основі моделі тестових сценаріїв, які задовольняють певним критеріям покриття. Станом називається множина пар атрибутів та їх значень у вигляді . Постумовою називається скінченна множина присвоювань виду , де атрибут стану ; вираз над константами та атрибутами стану ; атрибутна функція, що обчислює значення виразу у стані . Шляхом в із стану в стан називається така послідовність станів та переходів , що для усіх . Історією на шляху значення атрибуту a в стані s є множина , яка складається із самого атрибуту a, або, якщо його значення перезаписувалося у постумові попереднього переходу, то всі атрибути, що містяться в правій частині відповідного присвоювання.У дисертаційній роботі розглянуто проблеми побудови точних абстракцій станів моделі, спрямованого пошуку поведінки моделі й генерації тестових сценаріїв на основі моделі, а також проблема автоматизації побудови формальних моделей. Метод повністю автоматичний, не потребує втручання з боку користувача, не суперечить методам часткового порядку, методам, які застосовують симетрії, а також може бути використаний сумісно із символьними методами абстракції предикатів, що будують абстракції до виконання перевірки моделі. Побудовано алгоритм верифікації, що реалізує метод побудови абстракцій станів моделі. Так, перевірка властивостей моделі у наведеному прикладі такими популярними системами верифікації як SMV, NUSMV, VCEGAR, BLAST, SPIN показала експоненційну складність (по часу та кількості станів, а у деяких випадках і по кількості ітерацій уточнень абстракцій). Автоматизована побудова формальної моделі дозволяє уникнути необхідності явного введення допоміжних атрибутів, зберегти компактність і структурованість вихідного опису моделі, що дозволяє суттєво зменшити обєми та підвищити якість формалізації, а також скоротити трудовитрати та час виконання задач верифікації в цілому.

ОСНОВНИЙ ЗМІСТ РОБОТИ