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

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

МАТВЄЄВА Людмила Євгенівна

УДК 51.681.3

АНАЛІЗ ТА ВЕРИФІКАЦІЯ MSC-СИСТЕМ ЗА ДОПОМОГОЮ

МЕРЕЖ ПЕТРІ

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

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

Автореферат

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

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

Київ – 2005

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

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

Науковий керівник: |

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

Кривий Сергій Лук’янович,

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

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

член-кореспондент НАН України,

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

Перевозчикова Ольга Леонідівна,

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

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

Гороховський Семен Самуїлович,

Національний університет “Києво-Могилянська академія”

Міністерства освіти та науки України,

старший науковий співробітник

Провідна установа: |

Київський національний університет імені Тараса Шевченка,

факультет кібернетики,

кафедра теорії та технології програмування

Захист відбудеться “_____” _______________200__ р. о (об) ______ годині на засіданні

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

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

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

ім. В.М.Глушкова НАН України.

Автореферат розісланий “_____” _____________200__ р.

Учений секретар

спеціалізованої вченої ради

СИНЯВСЬКИЙ В. Ф.

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

Актуальність теми. Системи програмного і технічного забезпечення зростають за розміром і складністю. Щоб дозволити розроблювачам проектувати системи, які, незважаючи на складність, працюють надійно, необхідні методи, що забезпечують точний опис системи і можливість аналізу її властивостей. Один із шляхів досягнення цієї мети – використання формальних методів. За останні 20 років формальні методи широко використовуються для специфікації, аналізу, верифікації та відповідного тестування програмних і технічних систем. Вони є базовими для аналізу й верифікації правильності і повноти проектованих специфікацій, для перевірки відповідного впровадження у процесі цього проектування. Використання формальних методів у процесі проектування не гарантує коректність апріорно, тому що вони верифікують формальну модель, а не реальну систему. Однак можуть значно поглибити розуміння розроблюваної системи, виявляючи і демонструючи протиріччя, двозначності та неповноту, що інакше можна було б не знайти. У багатьох роботах формальні методи включають стандартизовані мови специфікацій, такі як мова ESTELLE (Extended State Transition System), мова LOTOS (Temporal Ordering Specification) та інші, широко використовувані методи специфікації – кінцеві автомати, мережі Петрі і темпоральні логіки. Формальна специфікація й верифікація програмних і апаратних систем є одним із шляхів підвищення надійності проектованих систем, а також прискорення процесу проектування. Вони доповнюють традиційний процес створення і прогону тестових наборів, підвищуючи рівень якості вихідного продукту.

областях діяльності, пов'язаних з інформаційною індустрією, поява нового програмного продукту на ринку залежить значною мірою від швидкості його розробки. Скоротити час розробки, утримуючись у рамках визначеного бюджету і необхідної якості, можливо також за допомогою технології моделювання проектованої системи, для чого застосовуються такі інженерні мови як VHDL (Very High Speed Integrated Circuit Hardware Description Language), MSC (Message Sequence Chart), SDL(Specification and Description Language), UML (Unified Modeling Language). Крім того, модель майбутньої системи допомагає вже на стадії проектування без вкладання великих коштів у “пілотний” проект одержати уявлення про поведінку системи й уникнути дорогих помилок надалі, коли в написання коду вкладені значні сили. Така модель може потім піддаватися верифікації й аналізу за допомогою формальних методів, а також традиційному тестуванню. Інженери-розроблювачі, як правило, використовують мови (VHDL, MSC, SDL, UML і т.п.), призначені для розв’язання задач проектування, а тестувальники-верифікатори – формальні методи чи мови (математичної логіки, теорії автоматів, алгебраїчні, мережні і т.п.), за допомогою яких вирішуються задачі верифікації й аналізу. Оскільки інженери-розроблювачі і тестувальники-верифікатори використовують у своїй діяльності різні мовні засоби, це може призвести до неоднозначного розуміння тих самих фрагментів проекту, чи неточностям, навіть протиріччям у вихідних технічних вимогах і, нарешті, до неповноти описів. Виходом з такої ситуації є розробка автоматизованих інтерфейсів між мовами інженерів-розроблювачів і тестувальників-верифікаторів. Таким чином, проблема автоматизації процесів проектування, верифікації і тестування особливо актуальна, тому що виявлення помилок на ранніх стадіях розробки та їхнє усунення дозволяє продукцію зробити дешевшою, одержавши при цьому якісний продукт і виграш у часі. З одного боку, така автоматизація дозволяє уникати помилок у проектованій системі, привнесених за рахунок використання в рамках процесу побудови системи різними інженерами різних мовних засобів, з іншого – дозволяє інженерам-розроблювачам проектувати і тестувати систему, залишаючись у звичному для себе мовному середовищі. Це означає, що вердикт, сгенерований за результатами верифікації й аналізу, має бути представлений інженеру-розроблювачу в його робочому форматі, тобто мовою проектування системи.

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

Зв’язок з науковими програмами, планами, темами. Дисертаційна робота виконана в рамках наукової теми Інституту кібернетики ім. В.М. Глушкова НАН України: ВФ 100.05 “Розробка дедуктивних методів верифікації теорем з математики та програмного забезпечення ЄОМ”(державний реєстраційний номер 0102U000496).

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

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

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

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

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

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

- уперше побудовано Алгоритм Перекладу опису проектованої системи мовою MSC'2000 у мережі Петрі та доведена його коректність за допомогою алгебри процесів, а саме –бісімуляційна еквівалентність вхідних MSC діаграм та синтезованої за цими діаграмами мережі Петрі;

- у процесі доведення коректності Алгоритму Перекладу з MSC’2000 у мережі Петрі уперше визначена формальна семантика базового елемента мови MSC'2000 – <умова> (condition);

- розроблено та обґрунтовано оригінальні алгоритми аналізу і верифікації формальної моделі у вигляді мережі Петрі, що використовують метод TSS розв’язання систем лінійних однорідних і неоднорідних діофантових рівнянь над множиною натуральних чисел: а) алгоритм верифікації таких властивостей мереж Петрі – (структурна) обмеженість, L3-живість, досяжність, наявність дедлоків; б) алгоритм побудови S- і T-інваріантів мережі Петрі; в) алгоритм пошуку пасток і тупиків асиметричної мережі Петрі. Знижена обчислювальна складність аналізу динамічних властивостей мережі Петрі, який проводиться за допомогою розв’язання рівняння стану;

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

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

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

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

У спільних публікаціях за темою дисертації автору належать наступні результати: у роботі [5] – розробка алгоритму верифікації таких властивостей мережі Петрі: (структурна) обмеженість, L3-живість, досяжність; у роботі [6] – використання визначення інваріантності властивостей базової моделі для розробки методики виявлення конфліктів функціональностей проектованої системи, аналіз властивостей мереж Петрі та вибір моделі телефонної мережі для експериментального застосування методики пошуку конфліктів функціональностей; у роботі [7] – аналіз існуючих формальних методів і методик пошуку та запобігання конфліктів функціональностей систем, розробка й обґрунтування алгоритму виявлення конфлікту функціональностей проектованої системи на базі визначення інваріантності властивостей базової моделі у вигляді мережі Петрі та результати експериментів; у роботі [8] – розробка алгоритму побудови S- і T-інваріантів мережі Петрі; у роботі [9] – побудова Алгоритму Перекладу з мови MSC’2000 у мережі Петрі; у роботі [10] – обґрунтування Алгоритму Перекладу з мови MSC’2000 у мережі Петрі; у роботі [11] – розробка повністю автоматизованої технологічної лінії аналізу властивостей формальної моделі проектованої MSC-системи за допомогою розв’язання систем лінійних рівнянь та експериментальне застосування цієї лінії; у роботі [12] – покроковий опис єдиного автоматизованого технологічного процесу аналізу та верифікації проектованої системи у вигляді набору діаграм мови MSC’2000 та обґрунтування етапів процесу.

Апробація результатів роботи. Основні наукові і практичні результати даної роботи доповідалися на Міжнародному симпозіумі "Питання Оптимізації Обчислень – ХХХ." (Кацивелі, Крим, 2127 вересня 2001); Українському математичному конгресі – 2001. Секція 13 “Математична теорія керування”, Інститут математики НАН України, Київ, 21–23 серпня 2001; 2-й Міжнародній науково-технічній конференції “Штучний Інтелект”, 1–6 жовтня 2001, Росія, Таганрог; 3-й Міжнародній науково-технічній конференції “Штучний Інтелект”, 16–20 вересня 2002, Кацивелі, Крим; 3-й Міжнародній конференції по програмуванню Укрпрог'2002, Київ 21–23 травня 2002 р. Інститут кібернетики ім. В.М.Глушкова НАН України; 4-й Міжнародній конференції по програмуванню Укрпрог'2004, Київ 1–4 червня 2004 р., Інститут кібернетики ім. В.М.Глушкова НАН України; Міжнародній конференції "Алгебра, логіка і кібернетика" (Алик-2004), Росія, Іркутськ, 25–28 серпня 2004; 10-th International conference “Knowledge, Dialog, Solution” (KDS’2003), Varna, Bulgaria, 16–26 June, 2003; SCI 2003 (7th World Multi-Conference on SYSTEMICS, CYBERNETICS AND INFORMATICS), USA, Orlando, 27–30 July 2003; ICINCO’2004 (International Conference on Informatics in Control, Automation and Robotics), August 25–28, Setъbal, Portugal, 2004; Workshop “Concurrency, Specification and Programming CS&?'2004”, Germany, Caputh, September 24–26, 2004.

Публікації. За темою дисертації опубліковано 12 наукових праць, причому 7 із них – статті у фахових виданнях наукових праць, 5 – публікації в матеріалах науково-практичних конференцій. Усі роботи наведені в списку літератури.

Обсяг та структура роботи. Дисертація складається із вступу, шести розділів, висновку, списку літератури з 162 найменувань і додатка. Загальний обсяг дисертації – 158 сторінок, обсяг основного тексту дисертації 141 сторінка.

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

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

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

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

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

Означення 1. Мережею називається трійка , де і – деякі непусті множини, елементами яких є відповідно місця і переходи; – бінарне відношення інцидентності між місцями та переходами. На основі відношення інцидентності вводиться функція інцидентності , де — множина натуральних чисел.

Нехай – довільний елемент мережі. Для елемента визначимо множину його вхідних та вихідних елементів: і .

Для мережі необхідне виконання наступних умов:

С1) , С2) ,

С3) .

Означення 2. Розміткою мережі називається функція .

Означення 3. Мережа Петрі (МП) – це набір , де – деяка мережа; – деяка початкова розмітка мережі ; W – функція, що називається кратністю дуг та ставить у відповідність кожній дузі МП число n>0. МП називається ординарною, якщо кратність всіх її дуг рівна 1.

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

Означення 5. Додатні цілочислові розв’язки однорідної системи лінійних діофантових рівнянь , похідної від рівняння стану, називаються Т-інваріантами мережі Петрі. Додатні цілочислові розв’язки однорідної системи лінійних діофантових рівнянь називаються S-інваріантами мережі Петрі, де – транспонована матриця інцидентності.

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

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

Четвертий розділ є основним у даній роботі. Він містить детальний опис даного технологічного процесу з обґрунтуванням та використанням прикладів.

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

· переклад опису проектованої системи у вигляді набору діаграм мови MSC'2000 у мережу Петрі;

· аналіз властивостей формальної моделі, одержаної внаслідок такого перекладу;

· верифікація даної формальної моделі;

· виявлення конфлікту функціональностей проектованої MSC-системи;

· модифікація/виправлення проектованої MSC-системи.

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

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

На сьогодні робота з розв’язання задачі перекладу діаграм MSC у мережі Петрі ведеться різними дослідниками, котрі розробляють семантику для стандартів MSC'96 і MSC'2000, засновану на мережах Петрі, а також працюють над перетворенням діаграм у мережі. Однак автоматичний переклад ними не розглядається. Крім того, у них відсутній такий переклад елементу мови MSC'2000 <умова> (condition), що був би коректним з погляду семантики цього елемента.

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

Теорема 8. Вихідні MSC діаграми та синтезована за цими діаграмами мережа Петрі, побудована у відповідності до Алгоритму Перекладу, (строго) бісімуляційно еквівалентні.

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

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

Твердження 1. Наявність в ординарній мережі Петрі таких структурних властивостей як структурна обмеженість, (часткова) повторюваність, (часткова) несуперечливість, L3-живість, консервативність, контрольованість можна визначити, обмежившись тільки аналізом S- та T- інваріантів мережі Петрі.

рамках даного технологічного процесу розроблено з реалізацією деяких фрагментів ряд оригінальних алгоритмів аналізу і верифікації формальної моделі у вигляді мережі Петрі, що використовують метод TSS розв’язання систем лінійних однорідних і неоднорідних діофантових рівнянь над множиною натуральних чисел: а) алгоритм верифікації структурних властивостей мереж Петрі; б) алгоритм побудови S- і T-інваріантів мережі Петрі.

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

Твердження 2. Усічена множина розв’язків (TSS) системи лінійних однорідних діофантових рівнянь представляє мінімальну породжуючу множину інваріантів мережі Петрі, яка визначається даною системою рівнянь.

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

Теорема 9. Задача перевірки сумісності рівняння стану зводиться до задачі перевірки на рівність нулю добутків усіх його S- інваріантів і різниці кінцевої та початкової розміток даного рівняння стану.

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

Ілюстрація однієї з ліній запропонованого технологічного процесу – переклад та наступний аналіз моделі з видачею вердикту аналізу, виконується на прикладі з області телекомунікації. Розглядається реальна телефонна система, яка складається з базових сервісів і традиційно називається Plain Old Telephony Service або Plain Old Telephony System, POTS. Цей експеримент підтверджує доцільність та ефективність використання описаного технологічного процесу для аналізу і верифікації розподілених систем.

Представлена в даній роботі технологія може застосовуватися не тільки для розв’язання задачі верифікації чи аналізу, але й для розв’язання задачі синтезу системи – нарощування її функціональних можливостей. Розв’язується задача визначення й усунення конфліктів функціональностей (Feature Interaction (FI)) у телекомунікаційній системі. Останнє десятиліття характерне інтенсивним застосуванням формальних методів для визначення і розв’язання проблеми FI. Однак на сьогодні єдиного підходу до розв’язання проблеми FI не існує. Визначення й усунення FI є складною і важкою задачею, і донедавна в телефонній індустрії задачі FI визначалися й розв’язувалися в основному частково автоматизованими ручними методами. У даній роботі представлена оригінальна методика пошуку конфліктів функціональностей проектованої системи за допомогою інваріантності властивостей базової моделі. Введене в даній роботі означення інваріантності властивостей базової моделі дозволяє побудувати і реалізувати ефективний алгоритм виявлення конфлікту функціональностей.

Означення 7. Нехай – множина виділених властивостей та T-інваріантів деякої вихідної мережі Петрі , – множина властивостей та T-інваріантів мережі Петрі , яка моделює систему, побудовану з базової системи та деякого додаткового сервісу (або властивості) . Модель назвемо інваріантною щодо функціональних властивостей базової моделі , якщо з точністю до іменування переходів і місць та розмірності простору T-інваріантів. Модель має FI стосовно базової моделі , якщо має місце .

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

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

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

· процес дозволяє багатоцільове й інтегроване використання;

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

· ефективність застосування, можливість порівняно швидко обробляти великі системи;

· практичність застосування, що безпосередньо випливає з того, що процес автоматизований;

· відкритість” системи, можливість нарощування функціональних можливостей;

· можливість настроювання на пошук заданого класу помилок проектованої системи.

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

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

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

Сьомий розділ містить висновки даної роботи.

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

ВИСНОВКИ

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

- уперше побудовано Алгоритм Перекладу опису проектованої системи мовою MSC'2000 у мережу Петрі;

- уперше розширена стандартизована формальна семантика мови MSC'2000 за рахунок доповнення її формальною семантикою елементу мови MSC'2000 <умова>;

- доведено коректність Алгоритму Перекладу за допомогою алгебри процесів – бісімуляційна еквівалентність вхідних MSC діаграм та синтезованої за цими діаграмами мережі Петрі;

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

- доведено коректність усіх кроків даного технологічного процесу;

- у ході реалізації процесу були розроблені й реалізовані оригінальні алгоритми: побудови S- і T-інваріантів мережі Петрі та пошуку пасток і тупиків класу асиметричних мереж Петрі;

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

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

Достовірність результатів дисертації випливає з логічності та строгості математичних доведень теорем та тверджень і підтверджена результатами експериментів.

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

1. Матвеева Л.Е. Спецификация и верификация некоторых свойств динамических систем // Комп`ютерна математика. Оптимізація обчислень. – Київ, 2001.–Том 1. – С. 281–292.

2. Матвеева Л.Е. Анализ сетей Петри с помощью инвариантов // Искусственный интеллект.– 2001.– №3.– С. 243–250.

3. Матвеева Л.Е. Формальное представление и анализ свойств асинхронных динамических систем // Проблемы программирования.–2002.–№1–2.– С.168–174.

4. Матвеева Л.Е. Автоматическая система анализа и верификации телекоммуникационной системы, описанной на языке MSC, с помощью формализма сетей Петри // Проблемы программирования.–2004.–№2–3.– С.108–117.

5. Крывый С.Л., Матвеева Л.Е. Об одном методе анализа сетей Петри // Матеріали Укр. мат. конгресу – 2001. Секція 13 “Математична теорія управління”.– К.: Ін-т математики НАН України, 2001.– С.24–25.

6. Крывый С.Л., Матвеева Л.Е. О применении сетей Петри к решению некоторых задач телекоммуникации // Искусственный интеллект.–2002.–№3.– С.590–598.

7. Крывый С.Л., Матвеева Л.Е. Формальные методы анализа свойств систем // Кибернетика и системный анализ.–2003.– №2.– С.15–36.

8. Крывый С.Л., Матвеева Л.Е., Лопатина М.В. Алгоритм Построения TSS-множества для СЛОДУ в натуральных числах // "Алгебра, логика и кибернетика" (АЛиК-2004), матеріали Міжнародної конференції, яка присвячена 75-річчю з дня народження А.І. Кокоріна, Росія, Іркутськ, 25–28 серпня, 2004.– С.169–171.

9. Kryvyy S., Matvyeyeva L., Lopatina M. Automatic Translation of MSC Diagrams into Petri Nets // Intern. J. “Information Theories & Applications”. –2003. – 10, N 4.– P.423–430.

10. Kryvyy S., Matvyeyeva L., Lopatina M. Automatic Transformation of MSC Diagrams into Petri Nets // Proc. SCI’2003, Orlando, USA, 29-31 July 2003.–2003.– 5.– P.140–146.

11. Kryvyy S., Matvyeyeva L., Lopatina M. Automatic Analysis and Verification of MSC-specified Telecommunication System // ICINCO’2004 August (25-28) in Setъbal/Portugal. Proc. of First Intern. Conf. on Informatics in Control, Automation and Robotics.–2004.– 2.– P.402–405.

12. Kryvyy S., Matvyeyeva L., Lopatina M. Automatic Modeling and Analysis of MSC-specified Systems // Workshop “Concurrency, Specification and Programming CS&P’2004”, Caputh, September 24–26. Berlin, Humboldt-Universitдt zu Berlin, 2004.– 1. Petri Nets and Automata.– P.52–62.

АНОТАЦІЯ

Матвєєва Л.Є. Аналіз та верифікація MSC- систем за допомогою мереж Петрі. – Рукопис.

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

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

Загалом в роботі отримані такі результати: побудована низка алгоритмів, що разом складають єдиний автоматизований технологічний процес формальної специфікації та верифікації властивостей програмної (чи апаратної) системи, причому вхідною та вихідною мовами даного процесу є мова інженерного моделювання MSC’2000, доведена коректність алгоритмів, які входять до даного процесу. Зокрема, в роботі побудовано Алгоритм Перекладу з мови MSC’2000 у мережі Петрі, доведена коректність цього алгоритму за допомогою алгебри процесів; розроблені алгоритми верифікації наступних властивостей: (структурна) обмеженість, L3-живість, досяжність, наявність тупиків; розроблені та реалізовані оригінальні алгоритми побудови S- і T- інваріантів та пошуку пасток і тупиків асиметричних мереж Петрі; створена методика пошуку конфліктів функціональностей проектованої системи на основі поняття інваріантності властивостей базової моделі.

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

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

АННОТАЦИЯ

Матвеева Л.Е. Анализ и верификация MSC- систем с помощью сетей Петри. – Рукопись.

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

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

В целом в работе получены следующие результаты: построен ряд алгоритмов, которые вместе составляют единый автоматизированный технологический процесс формальной спецификации и верификации свойств программной (или аппаратной) системы, причём входным и выходным языком данного процесса является инженерный язык моделирования MSC’2000, доказана корректность алгоритмов, которые входят в данный процесс. В частности, в диссертации построен Алгоритм Перевода с языка MSC’2000 в сети Петри, доказана корректность этого алгоритма с помощью алгебры процессов; разработаны алгоритмы верификации следующих свойств: (структурная) ограниченность, L3-живость, достижимость, наличие тупиков; разработаны и реализованы оригинальные алгоритмы построения S- і T- инвариантов и поиска ловушек и тупиков сетей Петри; создана методика поиска конфликтов функциональностей проектируемой системы на основе понятия инвариантности свойств базовой модели.

Работа всех алгоритмов иллюстрируется соответствующими экспериментами, которые демонстрируют корректность алгоритмов и всей методики в целом.

Ключевые слова: MSC’2000, автоматический перевод, верификация, сети Петри, алгебра процессов, семантика, формальные методы, линейная алгебра, формальная спецификация.

ABSTRACT

Matvyeyeva Lyudmila E. Analysis and verification of MSC-specified system by means of Petri nets. – Manuscript.

Thesis for the degree of the Candidate of Physics and Mathematics. Speciality 01.05.03. – Mathematical and Software Support of Computers and Systems. – V. Glushkov Institute of cybernetics of National Academy of Science of Ukraine. – Kyiv, 2005.

Formal specification and verification of the software and hardware systems is one of the approaches to improve reliability of the systems under design, to speed up their design process. A real system undergoes formalization in the following way. Firstly, the system properties for analysis are identified. Then they are formally specified as a formal model which undergoes verification. Finally, different verification tools are used to prove whether or not the model meets the required functionality of the system. Automation of these processes during design phase of either hardware or software system is extremely important task in order to deliver a high-quality product. The development-engineers and testers (verifiers) utilize different languages in their work that usually leads to the different interpretation of the same functionality, to uncertainty or even to inconsistencies in original requirements or incompleteness of the requirements. The way out of this situation is the development of automatic interfaces between languages of development-engineers and testers (verifiers).

The following problem is resolved in this thesis: technological process is build to analyse and verify software or hardware system specified in MSC’2000 language. The main properties of the process are the following: the process is fully automatic; input language and language of the output verdicts are an operating languages of development-engineers, so far do not require specific mathematical background.

As the formal model the system utilizes ordinary Petri net because of their profound support for analysis of many properties and problems associated with concurrent systems – the most difficult in manual testing. Given work is based on well-known definitions of Petri nets theory, and classical definitions of incidence matrix, the state equation and Petri net invariants.

The algorithm of the translation of a set of MSC diagrams, which describes the system under design, into Petri net is presented. The algorithm works over the selected subset of basic MSC’2000 elements. MSC is a modelling technique that uses a graphical interface, which was standardized by ITU (International Telecommunication Union). It is usually applied to reactive distributed real-time systems, often in combination with SDL language. These very properties of the systems make an MSC, with possibility of scenario describing, extremely suitable as for specification purposes. The proof of the algorithm correctness is based on the use of process algebra ACP. Namely, the bisimular equivalence of the input set of MSC diagrams and output Petri net is proved. The most significant feature of the given algorithm is the way of handling