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

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

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

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

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

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

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

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

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

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

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

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

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

Література:

1. Паралельні бази даних [Електронний ресурс].–Режим доступу:\www/URL: http://www.simulation.kiev.ua/dbis/lection27.html – 10.05.2015. – Загол. з экрану.

2. Паралельні обчислення [Електронний ресурс].–Режим доступу:\www/URL: https://uk.wikipedia.org/Паралельні_обчислення – 16.05.2015. – Загол. з экрану.