Маслійчук О.В.

Черкаський національний університет ім. Богдана Хмельницького

Моделювання та верифікація розподілених процесів за допомогою недетермінованих кінцевих автоматів

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

За останні роки багато аварій та катастроф виникло саме через помилки у програмному забезпеченні. Так 4 квітня 1996 р. при першому запуску на 39-й секунді після старту вибухнула ракета ’Аріан 5’, яка була створена і випускається зараз Європейською космічною агенцією. Бортова система цієї ракети використовувала ПЗ попередньої версії ’Аріан 5’, але архітектура апаратної частини була змінена. Після ретельного дослідження було встановлено помилку у навігаційній програмі. Втрати були величезними. 28 травня 2008 р. NASA втратила зв’язок з марсоходом ’Фенікс’, виконання завдань були відкладені [1]. І в цьому випадку втрати були значними. На жаль, таких прикладів багато ще можна навести. Тому актуальність роботи у напрямку розробки коректного програмного забезпечення з одночасною його верифікацією та подальшого безпосереднього створення програми не викликає сумнівів. Особливо це важливо для розподілених систем, де інформація може з’являтись у поточну частину програми несподівано і незалежно від цієї програми через переривання.

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

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

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

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

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

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

Література:

1. Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем.–СПб.:БХВ–Петербург,2010.–560c.