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

Размещено на http://www.allbest.ru/

Національна академія наук України Інститут кібернетики імені В.М. Глушкова

УДК 519.686.2

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

01.05.03 математичне та програмне забезпечення обчислювальних машин і систем

Автореферат

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

Колчин Олександр Валентинович

Київ 2009

Дисертацією є рукопис.

Робота виконана в Інституті кібернетики імені В.М. Глушкова НАН України.

Науковий керівник: доктор фізико-математичних наук, професор,

академік НАН України

Летичевський Олександр Адольфович,

Інститут кібернетики імені В.М. Глушкова НАН України,

завідуючий відділом

Офіційні опоненти: доктор фізико-математичних наук, професор

Дорошенко Анатолій Юхимович,

Національний технічний університет України

«Київський політехнічний інститут»,

кандидат фізико-математичних наук, доцент

Гороховський Семен Самуїлович, Національний університет ''Києво-Могилянська академія''

Захист відбудеться 12.06. 2009 р. о(об) 11 годині на засіданні спеціалізованої вченої ради Д 26.194.02 при Інституті кібернетики імені В.М. Глушкова НАН України за адресою: 03680, МСП, Київ-187, проспект Академіка Глушкова, 40.

З дисертацією можна ознайомитися в науково-технічному архіві інституту.

Автореферат розісланий 05.05.2009 р.

Учений секретар спеціалізованої вченої ради СИНЯВСЬКИЙ В.Ф.

автоматизація формальний асинхронний

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Із зростанням складності програмних систем загострюється актуальність автоматизації перевірки їх правильності. Вимоги, що висуваються до якості, стають все більш критичними, адже все частіше автоматизуються системи керування машин, від функціонування яких залежать не тільки прибутки підприємств, але й життя людей сучасні програмні системи активно використовуються у системах управління польотами, автомобілях, медичному обладнанні. Паралельність і асинхронність є природними рисами практично всіх сучасних програмних комплексів. При цьому багато дослідників вважають їх самими складними й заплутаними створеннями людини. Методи тестування не забезпечують вичерпного аналізу усіх можливих варіантів поведінки, тим самим не можуть гарантувати відсутність порушень властивостей, якими мають володіти системи, що розроблюються. Для систем зі складною поведінкою моделі стає неможливим обходитися без автоматизації перевірки правильності верифікації. Одним з основних методів верифікації є перевірка формальних специфікацій моделі (model checking). Моделі, що перевіряються, представляються у вигляді графа переходів станів, а властивості формулюються у темпоральній логіці. Останнього часу метод широко використовується для перевірки властивостей повноти, несуперечливості і безпеки специфікацій як програмного, так і апаратного забезпечення промислових систем.

Основною проблемою верифікації є комбінаторний вибух числа станів моделі. Досвід виконання робіт з верифікації сучасних промислових систем показує, що оціночна кількість досяжних станів, як правило, перевищує . Очевидно, що за такої кількості станів перевірка моделі шляхом їх наївного перебору практично нездійсненна. Вирішенню проблеми присвячено багато різних технологій розроблені методи часткового порядку для елімінації надлишкового інтерлівінгу, використовуються симетрії при перевірці еквівалентності станів, досліджуються інформаційні залежності, застосовуються техніки абстракції, факторизації, апроксимації, символьного моделювання. До процесу верифікації активно залучений користувач (експерт предметної області) його "підказки" використовуються для спрямованого пошуку, побудови абстракцій, накладання обмежень на простір пошуку. Використовуються симулятори, інтерактивні режими та ін. Однак існуючі методи мають ряд недоліків, і, на жаль, на сьогодні не існує прийнятного для промисловості вирішення даної проблеми. Методи побудови абстракцій погано автоматизуються, часто приводять до хибних результатів, котрі потребують уточнень, і як наслідок повторних запусків експериментів. Критерії для завершення процесу уточнень, як правило, основані на евристиках або вимагають участі експерта. Статичні методи виявлення залежностей перебільшують фактичні інформаційні зв'язки, що відображується на ефективності абстракцій. Тому актуально створення автоматичного методу оперативної побудови точних абстракцій станів моделі, мета якого значне зменшення часу та пам'яті, необхідних для перевірки властивостей моделі.

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

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

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

Об'єкт дослідження транзиційні системи, формальні моделі паралельних асинхронних систем, автоматичні методи перевірки властивостей моделей.

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

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

Наукова новизна результатів.

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

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

Практичне значення отриманих результатів.

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

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

- Розроблено новий програмний комплекс, який включає реалізацію запропонованих алгоритмів побудови абстракцій та спрямованого пошуку. Побудовано транслятори сучасних інженерних мов специфікацій MSC і SDL, UML Statecharts, а також напівформальних табличних і текстових описів поведінки систем у формальну модель. Автоматизація побудови формальних моделей дозволяє значно підвищити якість формалізації та скоротити час виконання задач по верифікації в цілому. Розглянуті у дисертації алгоритми та методи впроваджено у промислову розробку систему VRS.

Зв'язок роботи з науковими програмами, темами. Робота виконувалась у рамках тем Інституту кібернетики ім. В.М. Глушкова: «Розробити методи та засоби продукування і маніпулювання знаннями у операційному середовищі інтелектуалізації інформаційних технологій», шифр ВФК.105.01, номер держреєстрації 0102U003204; «Розробити та дослідити ефективні методи специфікації та генерації безпечних систем у техногенному середовищі», шифр В.Ф.100.08, номер держреєстрації 0108U000105; «Розробити теорію та методи інерційного моделювання та верифікації багаторівневих взаємодіючих систем», шифр В.Ф.105.03, номер держреєстрації 0108U000106, а також у рамках проекту VRS (Verification Requirements Systems) «Верифікація вимог до систем», що виконується у компанії «Інформаційні програмні системи» сумісно з Інститутом кібернетики ім. В.М. Глушкова НАН України та компаніями Motorola і HengSoft (США).

Апробація результатів. Результати досліджень докладались та обговорювались на Міжнародних конференціях: «Ломоносов 2003» (Москва, Росія, 2003); конференції, прис-вяченої 110-річчю винаходу радіо (Санкт-Петербург, Росія, 2005); “Искусственный интеллект-2006. Интеллектуальные и многопроцессорные системы-2006” (Кацивелі, Крим, 2006); "Теоретичні і прикладні аспекти побудови програмних систем" (Київ, 2006); “Искусственный интеллект-2007. Интеллектуальные системы ИИ-2007” (Дивноморське, Краснодарський край, Росія, 2007); "Теоретичні і прикладні аспекти побудови програмних систем" (Бердянськ, 2007); ”УкрПрог 2008” (Київ, 2008); “Искусственный интеллект-2008. Интеллектуальные системы ИИ-2008” (Кацивелі, Крим, 2008). Отримані результати були темами на семінарах відділу теорії цифрових автоматів Інституту кібернетики ім. В.М. Глушкова НАН України та лабораторії GSG компанії Motorola (Санкт-Петербург, Росія).

Крім того, створений в компанії “Інформаційні програмні системи” на основі досліджень програмний комплекс було успішно апробовано у 9 промислових телекомунікаційних і телематичних проектах компанії Мotorola.

Публікації. Основні положення та результати опубліковано у 9 роботах, загальним обсягом 64 с., із них 5 у наукових фахових виданнях, затверджених ВАК України, 4 у працях науково-практичних конференцій.

Особистий внесок. Всі зазначені результати отримані автором самостійно. В роботах, виконаних у співавторстві, О.В. Колчин вніс такий вклад: у роботі [7] описаний трасовий генератор, розроблені та побудовані відповідні алгоритми та модуль програмного комплексу; у роботах [1, 2] викладена загальна методика створення формальних моделей мовою базових протоколів, запропоновані методи введення допоміжних атрибутів та операцій над ними для збереження семантики вихідних моделей.

Структура та обсяг роботи. Дисертація складається із вступу, чотирьох глав, висновку, списку літератури із 180 найменувань і двох додатків. Основний зміст складає 120 сторінок, обсяг додатків 5 сторінок. Робота містить 21 ілюстрацію і 3 таблиці.

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

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

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

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

У розділі 1.1 наведені властивості формальних моделей, що перевіряються. Типовими поширеними помилками у моделях більшості програмних і апаратних систем, як правило, є: вихід за межі припустимих значень; переповнення і втрата значущості (over/underflow); ділення на нуль; використання не ініціалізованих атрибутів; неоднозначна реакція на зовнішні сигнали; недосяжна функціональність; тупики, а також порушення умов безпеки та живості поведінки системи, сформульованих для перевірки. Описана семантика логіки LTL, котра використовується для виразу лінійних темпоральних властивостей, які перевірятимуться.

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

Розділ 1.3 присвячено властивості лівлок. Наведені приклади моделей, які містять в собі лівлок, описані визначення та методи виявлення у різних роботах. Обґрунтовано метод перевірки властивості живості (відсутність лівлоків) перевірка здійснюється шляхом виявлення компонент сильної зв'язності графа поведінки моделі.

У розділі 1.4 наведено опис систем та методів створення тестових сценаріїв на основі формальних моделей. Зазвичай такі методи застосовують універсальні критерії покриття, використовуючи для генерації тестових сценаріїв лише перед- і постумови переходів та стани моделі. Деякі системи дозволяють описувати цілі тестів у вигляді послідовності повідомлень між інстанціями, що тестуються (наприклад, у вигляді MSC), або вимагають задавати формули темпоральної логіки над атрибутами моделі. Зазначається відсутність семантичної відповідності між тестовими сценаріями та основними функціональними специфікаціями до цільової системи.

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

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

Визначення 2.1. Станом називається множина пар атрибутів та їх значень у вигляді .

Визначення 2.2. Передумовою називається безкванторна формула логіки предикатів першого порядку над атрибутами множини та констант множини .

Визначення 2.3. Постумовою називається скінченна множина присвоювань виду , де атрибут стану ; вираз над константами та атрибутами стану ; атрибутна функція, що обчислює значення виразу у стані .

Визначення 2.4. Розміченим переходом називається трійка у вигляді , де передумова, мітка (ім'я) переходу, постумова.

Визначення 2.5. Атрибутною транзиційною системою (АТС) є вісімка у вигляді , де скінченна множина станів; початковий стан; скінченна множина розмічених переходів; скінченна множина міток; скінченна множина атрибутів; скінченна область значень для кожного атрибуту . Інтерпретація атомарних формул передумов задана функцією , де множина всіх атомарних формул із передумов , T та F відповідно означає «істина» та «хибність». Інтерпретація присвоювань у постумовах задана функцією , де множина усіх виразів із постумов .

За допомогою відношення задаються можливі варіанти дискретних детермінованих переходів із однієї множини станів в іншу, позначається якщо .

Визначення 2.7. Шляхом в із стану в стан називається така послідовність станів та переходів , що для усіх .

Визначення 2.8. Стан досяжний із стану , якщо існує шлях із в . Стан досяжний сам із себе. Множина всіх станів, досяжних із , позначається .

Визначення 2.9. Трасою в називається упорядкована послідовність така, що існує шлях .

Визначення 2.11. Конкретною АТС називається , у якій кожний стан системи є конкретним. Конкретний стан включає значення усіх атрибутів: .

Визначення 2.12. У абстрактній АТС кожний стан системи є абстрактним. Для кожного абстрактного стану існує така підмножина , що .

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

У розділі 2.2 наведено опис основних алгоритмів методу та їх обґрунтування. Основою служить алгоритм виявлення компонент сильної зв'язності Тарьяна та техніка «ледачих» обчислень. Логічні зв'язки передумов переходів та формул властивостей, що перевіряються, інтерпретуються як некомутативні, що дає можливість розрізняти «значущі» та «незначущі» значення атрибутів для кожного стану моделі. Алгоритм 2.4 формує абстрактні стани із значущих значень та їх історій. Історією на шляху значення атрибуту a в стані s є множина , яка складається із самого атрибуту a, або, якщо його значення перезаписувалося у постумові попереднього переходу, то всі атрибути, що містяться в правій частині відповідного присвоювання. Абстрактний стан вважається повністю сформованим, коли алгоритм завершує обхід сильно зв'язної компоненти графа, до якої він належить.

Лема 2.7 (сюр'єктивність абстракції). Кожному абстрактному стану відповідає щонайменше один конкретний досяжний стан: .

Лема 2.8 (функціональність абстракції). Одному конкретному стану відповідає тільки один абстрактний: .

Теорема 2.1 (бісимуляційна еквівалентність). Алгоритм 2.4 побудує таку абстракцію конкретної АТС, що .

Наслідок 1 (тотальність абстракції). Алгоритм побудує абстракцію для кожного досяжного конкретному стану: .

Наслідок 2 (трасова еквівалентність). Множини трас абстрактної та конкретної АТС збігаються.

Теорема 2.2. Алгоритм 2.4 побудує точну абстракцію конкретної АТС щодо властивостей , за час .

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

ТАБЛИЦЯ 1

Розмір задачі	SMV (стани)	NuSMV (пам'ять, Мбайти)	VCEGAR (стани)	BLAST (стани)	SPIN (стани)	Алгоритм побудови абстракцій (стани)
9	55.740	9	14.691	8.847.360	5.623	81
10	165.308	18	23.155	18.284.544	11.255	100
11	494.122	41	39.284	38.449.152	22.519	121
12	1.479.610	87	70.854	-	45.047	144
13	4.434.197	220	133.187	-	90.103	169
14	13.295.426	616	257.025	-	180.215	196

Результати експерименту демонструють екпоненційне зростання кількості станів (час роботи та об'єм пам'яті зростають пропорційно станам) верифікаторів SMV, NuSMV, VCEGAR, BLAST та SPIN, тоді як розробленого алгоритму квадратичне. Більше того, експоненційно зростає кількість ітерацій уточнень абстракцій у BLAST та VCEGAR, побудовані абстракції не покращують результат кількість станів зростає експоненційно.

Інший приклад має недосяжний перехід, у постумову якого входить інкремент деякого атрибуту c на константу z. Незважаючи на недосяжність, методи абстракції предикатів не мають прийнятного критерію для завершення побудови контр-прикладів (генеруватимуться предикати c > x, c + z > x, c + 2z > x,…); при обмеженні (c,x,z = 0..255) NuSMV повідомляє про помилку, намагаючись присвоїти змінній c значення 510; кількість станів (і, відповідно, час виконання) у експериментах з SMV, VCEGAR та BLAST значно скоротиться, якщо недосяжне присвоєння видалити. На відміну від згаданих верифікаторів, розроблений алгоритм не має залежності від постумов недосяжних переходів. У табл. 2 наведено результати експериментів перевірки таких моделей.



ТАБЛИЦЯ 2

Моделі	SMV (стани)	VCEGAR (стани)	BLAST (стани)	Алгоритм побудови абстракцій (стани)
з недосяжним переходом	106.705	304.564	3.330.194	11
без недосяжного переходу	9	738	404.928	11

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

Розділ 2.5 присвячено реалізації методу. Зазначено деякі оптимізаційні рішення, а також супутні техніки перевірки моделей, вироблені на основі досвіду використання програмного комплексу у промислових проектах.

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

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

перехід на максимальній дистанції ;

заборона переходу ;

де зразки конкатенація зразків;

де зразки недетермінований вибір зразків;

де зразки паралельна композиція зразків;

де зразок ітерація зразку , тобто .

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

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

Нехай зразок, який представляє мову над алфавітом множини , зразок, який представляє мову над алфавітом множини , . Тоді паралельна композиція зразків представляє мову над .

Побудована траса задовольняє зразкові, якщо вона містить переходи у послідовності, що не суперечить заданому зразку, на дистанціях, які не перевищують зазначені. Такі сценарії накладають додаткові обмеження на пошук, що служить інструментом для визначення напрямку пошуку. Для виявлення нескінченних циклів використовується ітерація (замикання Кліні). Наприклад, використовуючи ітерацію можна перевірити, чи приходить модель системи у сталий стан за відсутності зовнішніх сигналів.

У розділі 3.2 описано основний алгоритм генерації тестових сценаріїв та доведені його основні властивості. Згідно з теоремою 2.1 множини трас абстрактної та конкретної АТС збігаються, тому алгоритм 3.1 ґрунтується на модифікації алгоритму 2.4, де повні стани моделі являють собою добуток абстрактних станів АТС та станів автомата, який реалізує ціль тесту.

Теорема 3.1. Алгоритм 3.1 знайде всі траси, які задовольняють заданому зразку за час .

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

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

Четверта глава присвячена автоматизації побудови формальних специфікацій систем, що розроблюються. Описано внутрішню мову верифікатора мову базових протоколів (БП).

Визначення 4.1. Нехай АТС, а скінченна множина агентів (процесів). Тоді розподіленою (асинхронною) є така АТС , у якій множина міток представляє множину імен переходів, параметризованих ідентифікатором процесу: .

БП являють собою вирази у вигляді трійок Хоара: , де передумова, u подія, постумова. БП описують атомарні параметризовані переходи розподіленої АТС, параметром служить ідентифікатор агента (процесу). Таким чином, параметризований перехід може здійснюватись для будь-яких екземплярів процесу одного типу. Подія u використовується також для зберігання інформації про відповідну дію вихідної специфікації для відображення результатів у термінах вихідної моделі.

У розділі 4.2 стисло описані методи трансляції інженерних мов описання формальних моделей MSC, SDL та UML Statecharts у мову базових протоколів. Процеси та активні класи працюють асинхронно, що відповідає семантиці поведінки агентів у розподіленої АТС.

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

Додаток 1 описує статистику виконання робіт з верифікації промислових проектів. Додаток 2 містить опис моделей мовами популярних систем верифікації для прикладів з порівняльним аналізом.

ВИСНОВКИ

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

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

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

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

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

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

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

ОСНОВНІ ПОЛОЖЕННЯ ДИСЕРТАЦІЇ ОПУБЛІКОВАНО В ТАКИХ ПРАЦЯХ

1. Потиенко С.В. Представление SDL-спецификаций в виде базовых протоколов С.В. Потиенко, А.В. Колчин Искусственный интеллект. 2006. № 4. С. 42-52.

2. Потиенко С.В. Трансляция MSC сценариев в язык базовых протоколов С.В. Потиенко, А.В. Колчин Искусственный интеллект. 2007. № 3. С.428-435.

3. Колчин А.В. Разработка инструментальных средств для проверки формальных моделей А.В. Колчин Проблемы программирования. 2008. № 2-3. С. 622-626.

4. Колчин А.В. Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем А.В. Колчин Искусственный интеллект. 2008. № 3. С. 690-705.

5. Колчин А.В. Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем А.В. Колчин Проблемы программирования. 2008. № 4. С. 5-12.

6. Колчин А.В. Решение обыкновенных дифференциальных уравнений в системе компьютерной алгебры APS А.В. Колчин «Ломоносов 2003» междунар. конф. студентов и аспирантов, 17-19 апреля 2003 г. тезисы докл. М.: издательский отдел факультета ВМиК МГУ, 2003. С. 8-9.

7. Tools for requirements capturing based on the technology of Basic Protocols [Baranov S.N., Kapitonova J.K., Kolchin A.V. and oth.] Proc. of St. Petersburg IEEE Chapters. 2005. P. 92-97.

8. Колчин А.В. Альтернативные способы формализации требований А.В. Колчин Тео-ретичні та прикладні аспекти побудови програмних систем міжнар. конф., 5-8 грудня 2006 р., Київ. тези доп. К. НаУКМА [та ін.], 2006. С. 111-115.

9. Колчин А.В. Направленный поиск в верификации формальных моделей А.В. Колчин Теоретичні та прикладні аспекти побудови програмних систем міжнар. конф., 4-9 вересня 2007 р., Бердянськ. тези доп. К. НаУКМА [та ін.], 2007. С. 256-258.

АНОТАЦІЇ

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

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

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

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

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

Ключові слова: верифікація, транзиційна система, тестування, перевірка моделей.



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

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

С возрастанием сложности программных систем обостряется актуальность автоматизации проверки их правильности. В настоящее время программные системы активно используются в системах управления полетами, автомобилях, медицинском оборудовании. Параллельность и асинхронность являются естественными чертами практически всех программных комплексов. Методы тестирования не обеспечивают исчерпывающего анализа всех возможных вариантов поведения, тем самым не могут гарантировать отсутствие случаев нарушения свойств, которыми должны обладать разрабатываемые системы. Для систем со сложной моделью поведения становится невозможным обходиться без автоматизации проверки правильности верификации. Основной проблемой верификации является комбинаторный взрыв числа состояний модели. Работа посвящена созданию алгоритмов и методов для автоматической верификации формальных моделей больших промышленных систем.

Впервые получен метод оперативного построения точных абстракций состояний формальной модели для проверки темпоральных свойств. Главным отличием от существующих методов является то, что полученный метод строит точные абстракции, не нуждается в повторных запусках экспериментов для уточнений. Каждое абстрактное состояние формируется из подмножества атрибутов и их реальных значений соответствующего конкретного состояния, достаточного для проверки свойств модели. Таким образом, метод строит ослабленное отношение эквивалентности состояний. Построены алгоритмы, не ухудшающие асимптотическую сложность классических алгоритмов проверки темпоральных свойств; продемонстрирована эффективность по сравнению с существующими системами и методами верификации. За счет использования техники "ленивых" вычислений абстрактные состояния не различают варьирования значений незначимых атрибутов. Результаты экспериментов продемонстрировали на некоторых примерах понижение сложности выполнения проверки свойств модели с экспоненциальной до полиномиальной. Полная алгоритмизация, отсутствие необходимости во вмешательстве со стороны пользователя и в повторных запусках для уточнений абстракции, точность генерируемых результатов, а также сохранение реальных значений значимых атрибутов позволяет использовать созданный метод совместно с методами частичного порядка, методами, использующим симметрии, символьными методами абстракции предикатов, которые строят абстракции до осуществления проверки свойств модели и многими другими методами редукции пространства анализируемых состояний. Метод применим для проверки распространенных ошибок в моделях большинства программных и аппаратных систем, таких как выход за пределы допустимых значений, переполнение и потеря значимости, деление на ноль, обращение к неинициализированным атрибутам, неоднозначная реакция на воздействующие сигналы, недостижимость функциональности, тупики, а также нарушение условий безопасности и живости поведения системы, сформулированных для проверки пользователем в виде формул темпоральной логики.

Получено дальнейшее развитие методов направленного поиска поведений модели и автоматизации построения тестовых сценариев. Впервые в качестве направления используются специальные регулярные выражения над алфавитом имен переходов модели, позволяющие описывать как последовательную, так и параллельную композиции поведения процессов, а также использовать операции отрицания и недетерминированного выбора переходов, тем самым усовершенствовано задание целей тестирования. Операция итерации позволяет проверять нарушение специфических условий безопасности, например, наличие бесконечных циклов в поведении тестируемой инстанции при отсутствии внешних сигналов. Цели тестирования служат направлением для поиска, используются для отсечения несовместимых ветвей поведения модели и одновременно для проверки предполагаемого поведения на допустимость. При этом, по сути, осуществляется валидация модели. Описано применение метода для генерации на основе модели тестовых сценариев, удовлетворяющих заданным критериям покрытия, а также построения абстрактных трасс, в которых содержатся события только выделенных инстанций. Автоматизированное построение тестовых сценариев, обладающих необходимым уровнем покрытия, позволяет значительно уменьшить трудозатраты на анализ формальных моделей.

Разработан новый программный комплекс, включающий в себя реализацию описанных алгоритмов построения абстракций и направленного поиска. Построены трансляторы современных инженерных языков спецификаций MSC и SDL, UML Statecharts, а также полуформальных табличных и текстовых описаний поведения систем в формальную модель. Такой подход позволяет избежать необходимости явного введения вспомогательных атрибутов, сохранить компактность и структурированность исходного описания модели, что дает возможность существенно уменьшить объемы и повысить качество формальных моделей, сократить время выполнения задач верификации в целом. Рассматриваемые в диссертации алгоритмы и методы внедрены в промышленную разработку систему VRS. Созданный на основе исследований программный комплекс был успешно применен в 9 промышленных телекоммуникационных и телематических проектах.

Ключевые слова: верификация, формализация, транзиционная система, тестирование, проверка моделей.



Kolchin. Development a toolkit for checking of asynchronous models. Manuscript.

Thesis for a candidate degree on physics and mathematics (Ph.D.) by speciality 01.05.03 computer software. V.M. Glushkov Institute of Cybernetics of The National Academy of Sciences of Ukraine, Kiev, 2009.

A method for on-the-fly exact state abstraction construction for temporal properties checking obtained first. The main distinction with existing methods is that the obtained method does not need additional experiments runs because the abstract state consists of values of attributes subset, which is sufficient for the model properties checking. So the abstract states do not distinguish a variation of insignificant attributes values, this fact gives an opportunity to significantly decrease number of states needed for the properties checking.

A new method for guided search developed. At first a special regular expressions over alphabet of model transitions names are used as guides, and thus, the test goals specification improved. The method provides capability for automation of test scenario creation on a basis of formal model and thus gives an opportunity for decreasing of efforts needed for testing and model analysis.

A new software toolkit which incorporates the implementation of the described methods developed. Considered in the thesis algorithms and methods are applied in software industry the created toolkit has been applied in 9 industrial telecommunication and telematic projects.

Key words: verification, formalization, transition system, testing, model checking.

Размещено на Allbest.ru

...