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

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

Національна академія наук України

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

УДК 519.686.4

АВТОРЕФЕРАТ

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

Алгебраїчні методи верифікації асинхронних паралельних систем

01.05.03 - математичне та програмне забезпечення

обчислювальних машин і систем

Потієнко Степан Валерійович

Київ - 2009

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

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

Науковий керівник:доктор фізико-математичних наук, професор, академік НАН України Летичевський Олександр Адольфович, Інститут кібернетики імені В.М. Глушкова НАН України, завідуючий відділом.

Офіційні опоненти:

доктор фізико-математичних наук, професор Дорошенко Анатолій Юхимович, Національний технічний університет України «Київський політехнічний інститут»,

кандидат фізико-математичних наук, старший науковий співробітник Гороховський Семен Самуїлович, Національний університет «Києво-Могилянська академія».

Захист відбудеться 12.06.2009 р. о (об) 14годині на засіданні

спеціалізованої вченої ради Д 26.194.02 при Інституті кібернетики імені В.М. Глушкова НАН України за адресою:

03680, МСП, Київ-187, проспект Академіка Глушкова, 40.

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

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

Учений секретар спеціалізованої вченої ради Синявський В.Ф.

Загальна характеристика роботи

Актуальність теми. Застосування методів формального опису вимог є невід'ємною частиною сучасного процесу розробки складних програмних систем. Тестування не гарантує виявлення всіх помилок у продукті та не дає однозначної відповіді, чи відповідає продукт поставленим вимогам. Зважаючи на те, що обсяги і складність розробок постійно зростають, а кількість вимог досягає десятків тисяч, проблема автоматичної верифікації (перевірки правильності) набуває значної актуальності в індустріальних проектах. У цьому сенсі формальні методи мають найважливіше значення. Вони дозволяють створювати формальні вимоги й моделі поведінки систем з подальшою автоматичною верифікацією, генерацією програмного коду та набору тестів за заданими критеріями. Коректність отриманих результатів гарантується математичним апаратом, що опирається на досягнення алгебри, логіки і дискретної математики. Існує два загально відомих підходи до верифікації - це перевірка на моделі (model checking) і доведення теорем (theorem proving).

Перевірка на моделі - техніка, яка застосовується до моделей із скінченою множиною станів і перевіряє, що задані властивості виконуються на цій моделі. Тобто перевірка здійснюється як повний перебір простору станів, який має гарантовано закінчитися на скінченій моделі. Основна наукова проблема в цьому підході полягає у створенні ефективних алгоритмів і структур даних, що дозволять працювати з великими множинами станів. Це спричинено комбінаторним вибухом станів, що породжуються досліджуваними моделями. Відомі розробки в цьому напрямку - це Spin (використовує скорочення часткового порядку для зменшення вибуху станів), BLAST (використовує метод уточнень абстракцій на основі контрприкладів, також BDD), SMV (використовує BDD та абстракції предикатів), Murphі (використовує метод симетрій).

Доведення теорем являє собою техніку, в якій система та її властивості, що досліджуються, описуються як формули в певній математичній логіці. Така логіка визначається множинами аксіом і правил виведення. Процес перевірки моделі полягає у пошуку доведення формалізованих властивостей із набору аксіом. Деякі доведення можуть бути побудовані вручну, але актуальною науковою проблемою є автоматична побудова доведень. Основною задачею цього підходу є задача здійснимості бульових формул (SAT). До множини SAT пруверів належать системи Coq, Isabelle, HOL, LEGO, LCF та Nuprl, які використовувались для формалізації і розв'язання складних математичних задач у проектах верифікації програм. Всупереч перевірці на моделі, підхід доведення теорем може бути прямо застосований до моделей з нескінченою множиною станів.

Сучасні розробки поєднують перевірку на моделі з доведенням теорем, а також застосовують статичний аналіз (аналіз програмного коду або моделі системи без моделювання її поведінки) для побудови абстракцій та тверджень певної логіки з подальшими доведеннями. Такими розробками є PVS (символьна перевірка на моделі, автоматичні доведення з використанням BDD, техніка переписування), STeP (перевірка на моделі з інтерактивним доведенням теорем на базі BDD), SLAM (перевірка на моделі з використанням методу предикатних абстракцій), Bandera (аналіз анотованих Java програм, для доведення тверджень використовуються алгоритми Нельсона - Оппена), Verіsoft (аналіз програм на мовах C, C++, Java, використовується скорочення часткового порядку).

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

Зв'язок роботи з науковими програмами, темами. Робота виконувалась у рамках праць Інституту кібернетики імені В.М. Глушкова НАН України «Розробити методи інтелектуалізації інформаційних технологій для оптимізації паралельних обчислень і верифікації дедуктивними методами паралельних програм, що масштабуються» (шифр ВФК.105.02, номер держкеєстрації 0107U003570); «Розробити та дослідити ефективні методи специфікації та генерації безпечних систем у техногенному середовищі» (шифр В.Ф.100.08, номер держреєстрації 0108U000105); «Розробити теорію та методи інерційного моделювання та верифікації багаторівневих взаємодіючих систем» (шифр В.Ф.105.03, номер держреєстрації 0108U000106), а також у рамках проекту "Верифікація вимог до систем" виконуваного в компанії "Інформаційні програмні системи" разом з Інститутом кібернетики імені В.М. Глушкова НАН України і компаніями Motorola, Hengsoft.

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

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

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

Методи дослідження. Для вирішення поставлених задач застосовується парадигма алгебраїчного програмування, що реалізована в системі APS з мовою APLAN і базується на роботах Ю.В. Капітонової, О.А. Летичевського. Використовуються методи автоматичного доведення теорем та перевірки на моделі.

Наукова новизна отриманих результатів. Отримані результати є новими. Зокрема:

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

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

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

Особистий внесок здобувача. Всі наукові результати, викладені в дисертації, отримані автором особисто. В роботах, виконаних у співавторстві, С.В. Потієнко вніс такий вклад: у роботі [1] автором розроблено алгоритм нормалізації SDL моделі та трансляції конструкцій start, state, save, input, output, set, reset, timeout в мову базових протоколів; [2] - розроблено алгоритм трансляції керуючих конструкцій MSC alt, opt, exc, loop та par в мову базових протоколів та запропоновано розширення MSC сценаріїв анотаціями; [5] - розроблено алгоритми перевірки транзиційної повноти та несуперечливості базових протоколів, а також алгоритм перевірки коректності анотацій в MSC сценаріях; [6] - розроблено алгоритм анотаційного чекеру SDL специфікацій; [9] - створено опис середовища для верифікації MPI програм, а також синтаксис та семантику інтерпретації процесів у базових протоколах для формалізації функцій бібліотеки MPI.

Апробація результатів дисертації. Наукові та практичні результати доповідались та обговорювались на Міжнародних конференціях: "110 Anniversary of Radio Invention" (Санкт-Петербург, Росія, 2005), "Искусственный интеллект-2006. Интеллектуальные и многопроцессорные системы-2006" (Кацивелі, Крим, 2006), "Искусственный интеллект-2007. Интеллектуальные системы ИИ-2007" (Дивноморське, Краснодарський край, Росія, 2007), "Теоретичні та прикладні аспекти побудови програмних систем TAAPSD" (Київ, 2006, Бердянськ, Україна, 2007), "Моделирование устойчивого регионального развития" (Нальчик, Росія, 2007).

Реалізація розроблених алгоритмів включена до системи верифікації вимог, яка розвивається та використовується для роботи з вимогами у компаніях Motorola, Hengsoft, а також у компанії "Інформаційні програмні системи". Систему було успішно застосовано в 9 промислових проектах.

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

Структура та обсяг дисертації. Дисертаційна робота складається із вступу, основної частини з п'яти розділів, післямови, висновків та списку літератури із 65 джерел. Загальний обсяг дисертації 135 сторінок, основного тексту - 128 сторінок.

Основний зміст роботи

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

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

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

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

де S - множина станів, А - множина дій, - множина розмічених і нерозмічених (схованих) переходів, L - множина атрибутних розміток, - частково визначена функція розмітки станів.

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

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

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

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

.

тут f, f ' - формули базової мови, які задають стани системи до і після виконання базового протоколу.

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

Властивість несуперечливості системи базових протоколів визначається відсутністю перетинів передумов будь-яких протоколів з одним ключовим агентом:

де - передумови базових протоколів a_i і a_j, параметризованих списками x і y. Доведено наступне твердження.

Лема 1. Кожний агент несуперечливої системи має детерміновану поведінку.

Властивість повноти визначається наступним чином: диз'юнкція передумов базових протоколів з одним ключовим агентом має зводитися до істини:

,

де - передумова базового протоколу a_i, параметризованого списком x. Доведено твердження.

Лема 2. У повній системі відсутні тупики.

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

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

Теорема про коректність. Побудовані алгоритми мають такі властивості:

· скінченність: алгоритми завжди завершать свою роботу за скінченну кількість кроків;

· правильність: якщо знайдено порушення деякої властивості, то можна побудувати повну множину станів, у яких ця властивість не виконується;

· достатність: алгоритми достатні для перевірки того, що система володіє заданими властивостями (якщо порушень не знайдено, то модель не має досяжних станів, у яких ці властивості порушуються).

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

У додаток до алгоритмів статичної перевірки властивостей наведено два підходи до розв'язання проблеми досяжності. Перший полягає у здійсненні статичної фільтрації. Множина критичних станів розбивається на підмножини. Далі кожна підмножина з розбиття задається формулою базової мови і позначається c_i. Якщо розглянути заперечення цієї формули як умову цілісності і довести її виконання за допомогою розробленого алгоритму, то можна стверджувати, що критичні стани з даної підмножини недосяжні й можуть бути відфільтровані. Цей підхід дає можливість довести недосяжність деяких критичних станів. Для інших, не відфільтрованих, запропоновано наступний підхід, що базується на застосуванні методів перевірки на моделі. За допомогою таких методів можна спробувати довести досяжність заданих станів, але їх можливості обмежені із-за проблеми комбінаторного вибуху. Суть цього підходу полягає в автоматичному створенні певної абстракції конкретної системи, що перевіряється. Абстрагування здійснюється методом прихованих змінних та розбиття системи за типами агентів. Внаслідок цього, під час перевірки властивостей абстрактної системи не розглядається деяка множина атрибутів початкової системи, скорочується інтерлівінг агентів, що істотно зменшує множину станів системи. Це дає можливість побудувати повну, але надлишкову множину шляхів до заданих станів в абстрактній системі. Наведено метод використання цих шляхів для спрямованого пошуку в перевірці на моделі конкретної системи. програмний формальний асинхронний

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

У четвертому розділі побудовані прямий та зворотній предикатні перетворювачі, які використовуються як в алгоритмах статичної перевірки, так і в символьному моделюванні. Предикатний перетворювач - це функція перетворення однієї множини станів в іншу під дією заданого базового протоколу. Множини станів характеризуються формулами базової мови. В якості базової мови використовується мова багатосортного числення предикатів першого порядку. Формула базової мови може містити змінні та константи наступних простих типів: числові (цілий та дійсний) і символьні (булевський, злічений та довільний символьний). Також допускаються масиви елементів простих типів з цілими та зліченими індексами, функціональні типи (функції від аргументів простих типів, які повертають значення простого типу), списки елементів простих типів. У ролі змінних, що змінюють свої значення в процесі функціонування системи, виступають атрибути та атрибутні вирази. Останні є оператори доступу до елемента масиву за індексом (a[i₁,…,i_k]), функції доступу до списків (get_from_head(l), get_from_tail(l), empty(l)), вирази атрибутів функціональних типів (a(x₁,…,x_m)). Передумова базового протоколу містить формулу базової мови, постумова - оператори присвоювання, оператори оновлення списків (add_to_head(l,x), add_to_tail(l,x), remove_from_head(l), remove_from_tail(l)), а також формулу базової мови (позначимо її С). Лівими частинами присвоювань можуть бути атрибути простих типів та атрибутні вирази крім функцій доступу до списків. Присвоювання та оператори оновлення списків розглядаються як рівності, які пов'язують старі та нові значення атрибутів простих типів та атрибутних виразів. Будь-який виконуваний базовий протокол здійснює перехід: , де E і E' - формули, що визначають множини станів системи. Предикатні перетворювачі визначаються враховуючі наступне твердження: всі атрибути й атрибутні вирази, що зустрічаються на верхньому рівні у лівих частинах присвоювань, в операторах оновлення списків (крім другого параметра x) та на верхньому рівні в формулі С, і тільки вони можуть змінити свої значення після виконання базового протоколу. Вважається, що атрибут знаходиться на верхньому рівні, якщо він не міститься всередині будь-якого атрибутного виразу (наприклад, якщо атрибут зустрічається як індекс масиву або параметр атрибута функціонального типу, це не є верхнім рівнем).

На основі наведеної базової мови розроблено алгоритм прямого предикатного перетворювача, що із заданої множини станів E будує формулу E', яка визначає нову множину станів після виконання заданого базового протоколу:

,

де - перед- і постумови заданого базового протоколу.

Під час зворотного моделювання, навпаки, відома множина станів за формулою E' і необхідно побудувати формулу E, яка визначає попередню множину станів до виконання заданого базового протоколу. Для цього розроблено алгоритм зворотного предикатного перетворювача:

.

Доведено визначаючу властивість зворотного предикатного перетворювача:

.

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

,

де l - атрибут списочного типу, H і T - послідовності виразів, що визначають голову та хвіст списку відповідно, … - абстрактна (невідома) частина списку. Повністю абстрактним називається список з невідомою частиною і порожніми головою та хвостом: .

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

Стандарт діаграм послідовності повідомлень MSC розроблений Міжнародним союзом електрозв'язку (ITU-T) і входить до рекомендацій ITU-T серії Z.120. Діаграма MSC описує взаємодію скінченної множини інстанцій. Інстанціями позначаються абстрактні об'єкти, які можуть надсилати та приймати повідомлення, виконувати локальні дії, обробляти таймери, створювати інші об'єкти і виконувати зупинку. Всі події на одній інстанції упорядковані в часі й ніякі дві події не можуть бути виконані одночасно. В MSC не вводиться спеціального визначення глобального часу, інстанції працюють асинхронно. Для синхронізації різних інстанцій використовується конструкція condition. У даній роботі семантика цієї конструкції розширена передумовами (PRE /* <формула> */) та постумовами (POST /* <послідовність присвоювань і формула> */), які транслюються у відповідні конструкції базових протоколів, а також анотаціями (ANNO /* <формула> */), які перевіряються. Також підтримуються керуючі конструкції alt, opt, exc, par та loop для організації розгалуження та циклів. Конструкція reference транслюється з семантикою виклику функції. Послідовність виконання подій на інстанціях та коректне повернення із функцій здійснюється завдяки введенню додаткових атрибутів потоку керування.

Графічна мова опису і специфікацій SDL розроблена Міжнародним союзом електрозв'язку (ITU-T) і входить до рекомендацій ITU-T серії Z.100. Мова SDL включає описи як структурної, так і функціональної частин системи, що розробляється. SDL модель специфікується як множина взаємодіючих скінчених автоматів. Архітектура SDL моделі є багаторівневою. Об'єкт самого високого рівня називається системою (system), вона є структурним описом моделі. На інших рівнях моделі (всередині системи) розташовані блоки (block), які аналогічно системі є структурним описом. Вони можуть містити вкладені блоки і процеси, які є вже функціональним описом моделі. Взаємодія між процесами та з зовнішнім середовищем відбувається шляхом отримання та надсилання сигналів. Розроблений алгоритм трансляції SDL моделі в систему базових протоколів складається з двох основних етапів. Так як структурна частина мови базових протоколів є дворівневою - середовище із взаємодіючими в ній агентами, то на першому етапі здіснюється попередній аналіз і приведення системи до лінійного вигляду, яке називається нормалізацією SDL моделі. Далі кожен процес розглядається як агент і генерується опис середовища для майбутньої системи базових протоколів. На другому етапі транслюється необхідна підмножина конструкцій функціонального опису в базові протоколи.

Уніфікована мова моделювання UML була створена групою OMG у кінці минулого століття і стала загальною мовою для проектування та розробки програмного забезпечення. Вона складається з набору типів діаграм, які дають можливості опису програмної системи на різних рівнях та з різними цілями. За роки свого існування UML отримала широке розповсюдження в суспільстві інформаційних технологій, але до цього часу різні середовища моделювання використовують різні варіації UML, тим самим породжуючи свої стандарти. Одним з прикладів виступає компанія Telelogic з продуктом Tau G2. Виходячи з практичної необхідності зв'язку даної роботи з Tau, було обрано необхідну підмножину UML з деякими відмінностями від стандарту OMG та розроблено алгоритм трансляції UML моделей в мову базових протоколів. Так, Sequence Diagrams транслюються аналогічно MSC сценаріям. Для трансляції об'єктно орієнтованої структури пакетів і класів (Package Diagrams, Class Diagrams) розроблено алгоритм лінеаризації. Architecture Diagrams та State Chart Diagrams в Tau по суті є аналогами структурного та функціонального опису SDL відповідно. Тому алгоритми трансляції цих діаграм розроблено на базі алгоритмів нормалізації та подальшої трансляції SDL.

Висновки

У дисертаційній роботі отримані такі результати:

1) запропоновано формалізм базових протоколів для роботи з вимогами та надано можливості використання мов специфікацій MSC, SDL, UML як засобів створення і верифікації формальних моделей та вимог:

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

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

4) розроблено алгоритми прямого та зворотного предикатних перетворювачів як функцій перетворення однієї множини станів в іншу під дією заданого базового протоколу. Множини станів задаються формулами базової мови, яка є мовою багатосортного числення предикатів першого порядку з наступними типами змінних і констант: прості типи - числові (цілий та дійсний), символьні (булевський, злічений та довільний символьний), а також масиви елементів простих типів з цілими та зліченими індексами, функціональні типи (функції від аргументів простих типів, які повертають значення простого типу), списки елементів простих типів;

5) розроблено алгоритми трансляції певних підмножин інженерних мов специфікацій MSC, SDL та UML в мову базових протоколів з метою подальшої автоматичної верифікації. Підмножини цих мов було виділено виходячи з практичної необхідності в застосованих індустріальних проектах. Також було запропоновано розширення обраних мов для застосування методів верифікації у повній мірі: передумови, постумови та анотації у вигляді формул базової мови;

6) розроблено наступні алгоритми аналізу формальних вимог:

- алгоритм перевірки несуперечливості, повноти та властивостей цілісності систем базових протоколів;

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

- алгоритм трансляції обраних підмножин мов MSC, SDL та UML Statecharts із запропонованими розширеннями в мову базових протоклів.

7) розроблений автором програмний комплекс є важливою частиною системи верифікації вимог, яка розвивається та використовується для роботи з вимогами у компаніях Motorola, Hengsoft, а також у компанії "Інформаційні програмні системи".

Основні положення дисертації опубліковано в таких працях

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

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

3. Потиенко С.В. Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами / С.В. Потиенко // Проблеми програмування. - 2008. - № 4. - С. 39-45.

4. Потиенко С.В. Статическая проверка требований и подходы к решению проблемы достижимости / С.В. Потиенко // Искусственный интеллект. - 2009. - № 1. - С. 192-197.

5. Tools for requirements capturing based on the technology of basic protocols / [ Baranov S.N., Kapitonova J.K., Potiyenko S.V. and oth.] // Proc. of St. Petersburg IEEE Chapters. - 2005. - P. 92-97.

6. Потиенко С.В. Доказательство динамических свойств SDL-спецификаций в системе инсерционного программирования / С.В. Потиенко, А.А. Летичевский // Теоретичні та прикладні аспекти побудови програмних систем : міжнар. конф., 5-8 грудня 2006 р., Київ. : тези доп. - К. НаУКМА [та ін.]. - 2006. - С. 101-104.

7. Потиенко С.В. О подходах к решению проблемы времени в задачах верификации SDL систем / С.В. Потиенко, А.А. Летичевский // Теоретичні та прикладні аспекти побудови програмних систем : міжнар. конф., 5-8 грудня 2006 р., Київ. : тези доп. - К. НаУКМА [та ін.]. - 2006. - С. 124-128.

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

9. Летичевский А.А. Инсерционное моделирование и формализация библиотеки MPI / А.Ад. Летичевский, А.А. Летичевский, С.В. Потиенко // Моделирование устойчивого регионального развития : междунар. конф., 14-18 мая 2007 г., Нальчик. : пленарные доклады - Н. КБНЦ РАН [и др.]. - 2007. - С. 86-101.

Анотація

Потієнко С.В. Алгебраїчні методи верифікації асинхронних паралельних систем. - Рукопис.

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

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

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

Розроблений автором програмний комплекс входить до складу системи верифікації вимог, яка розвивається та використовується для роботи з вимогами у компаніях Motorola, Hengsoft, а також у компанії "Інформаційні програмні системи".

Ключові слова: транзиційні системи, агенти і середовища, формальні вимоги, верифікація, статична перевірка, суперечливість, повнота, цілісність, досяжність, предикатні перетворювачі, трансляція моделей, MSC, SDL, UML.

Аннотация

Потиенко С.В. Алгебраические методы верификации асинхронных параллельных систем. - Рукопись.

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

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

Существует два общеизвестных подхода к верификации - проверка на модели (model checking) и доказательство теорем (theorem proving). Проверка на модели применяется к моделям с конечным числом состояний и осуществляется как поиск в пространстве состояний. Основная проблема этого подхода лежит в построении и анализе большого пространства состояний, рост которого вызван эффектом комбинаторного взрыва. Доказательство теорем представляет собой технику, в которой и система и исследуемые свойства выражаются в виде формул в некоторой математической логике. Процесс проверки модели заключается в поиске доказательства выполнимости формул, построенных на основе заданных спецификаций.

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

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

Рассмотрена задача осуществления перехода системы от одного класса состояний к следующему под действием заданного базового протокола. Такая трансформация производится с помощью предикатных трансформеров. Построены алгоритмы прямого и обратного предикатных трансформеров, оперирующих над формулами базового языка. В качестве базового языка используется язык многосортного исчисления предикатов первого порядка. Формула базового языка может содержать переменные и константы следующих простых типов данных: числовые (целый и действительный) и символьные (булевский, перечислимый и произвольный символьный). Так же допустимы массивы элементов простых типов с целыми или перечислимыми индексами, функциональные типы (функции от аргументов простых типов, возвращающие значение простого типа), списки элементов простых типов. Предикатные трансформеры рассматриваются как функции, которые выводят из заданной формулы новую, определяющую класс состояний системы после перехода, совершенного под действием заданного базового протокола.

Ручная формализация спецификаций в виде базовых протоколов затрудняет процесс построения больших моделей, так как одним базовым протоколом описывается всего один (возможно, параметризированный) переход системы. Использование инженерных языков спецификаций MSC, SDL и UML существенно облегчает процесс формализации требований и дальнейшую работу над ними. Использование MSC позволяет описывать в одном сценарии альтернативы, условные операторы, циклы, недетерминизм, и не требует явного задания последовательности выполнения событий. Преимущество языка SDL в удобстве создания больших моделей. Он обладает такими востребованными и полезными для разработки свойствами, как наглядность и модульность, оснащен расширенным набором упрощающих описание вспомогательных конструкций. Язык UML создан относительно недавно с целью унификации разрабатываемых моделей и собрал в себе все преимущества MSC, SDL и других языков спецификаций и моделирования. Основываясь на практической необходимости из индустриальных проектов, были выделены подмножества языков MSC, SDL и UML, а так же предложены некоторые расширения, облегчающие верификацию моделей, описанных на этих языках. Разработаны алгоритмы трансляции выбранных подмножеств и расширений рассмотренных языков в язык базовых протоколов для дальнейшей автоматической верификации.

Автором разработаны программы и прототипы, реализующие алгоритмы, построенные в диссертационной работе. Реализация включена в систему верификации требований, которая развивается и применяется для работы с требованиями в компаниях Motorola, Hegsoft, а так же в компании "Информационные программные системы".

Ключевые слова: атрибутные транзиционные системы, агенты и среды, алгебра процессов, формальные требования, базовые протоколы, верификация, статическая проверка, противоречивость, полнота, свойства целостности, достижимость, предикатные трансформеры, трансляция моделей, MSC, SDL, UML.

Annotation

Potiyenko Stepan. Algebraic methods for verification of asynchronous parallel systems. - Manuscript.

Thesis for a candidate degree on physics and mathematics (Ph.D.) by speciality 01.05.03 - mathematical and software support of computing systems. - V.M. Glushkov Institute of Cybernetics of The National Academy of Sciences of Ukraine, Kyiv, 2009.

Methods of static analysis are developed for the systems represented in a form of basic protocols. Algorithms of checking properties of the system are built for consistency and completeness, satisfiability of safety conditions. Theorem about correctness of built algorithms is proved including statement that algorithms are enough to prove absence of formulated properties violations. The problem of search and reachability of states of the system where given properties broken is considered. Approaches to reachability problem solution are suggested using as static analysis as model checking methods. The task of system transition from one state class to the next by given basic protocol is considered. Such a transformation is realized by predicate transformers. In the current work, algorithms of forward and backward predicate transformers have been built for numeric and symbolic data types, functional data types, arrays and lists data structures. Transformers are considered as functions which derive from given formula a new one that defines state class of the system after transition made by given basic protocol.

Methods of creating formal specifications by means of engineering specification languages MSC, SDL and UML are proposed. Algorithms of model decomposition into basic protocols for further verification are developed. Such approach allows verifying high-level description languages and is aimed to simplify a process of formalization, analysis, modifications and review of formal model resulting in quality growth.

Software products and prototypes have been developed by author which implement algorithms built in this thesis. Implementations are included in system of requirements verification and used in Motorola and Hengsoft companies as well as in "Information Programming Systems" company.

Key words: attribute transition systems, agents and environments, process algebra, formal requirements, basic protocols, verification, static checking, consistency, completeness, safety properties, reachability, predicate transformers, model translation, MSC, SDL, UML.

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

...