Порядок опису і обробки графа автоматної моделі програми.

Анотація

У статті розглядається метод опису моделювання програм за допомогою предикатів, у результаті якого створюється модель у вигляді недетермінованого скінченного автомата. Пропонується формат опису предикатів із розділенням змістовної та умовною частин. Для опису змістовної частини предиката мають застосовуватись арифметичні оператори, дужки, стандартні функції та оператори темпоральної логіки U та N. Для логічної частини предикатів, крім логічних функцій, пропонується застосовувати також операції відношення і арифметичні оператори, дужки, стандартні функції. Формування опису кожного стану автоматної моделі програми має завершуватись розгалуженням по різних гілках моделі. Для опису моделей паралельних програм введені спеціальні стани: стан-монітор для доступу різних процесів до спільних ресурсів та стан-протокол для опису незалежних паралельних гілок. Модель створюється у процесі її опису, тому не потребує подальшої верифікації. Якщо опис моделі виконаний коректно і при цьому обраний оптимальний алгоритм майбутньої програми, то така модель повністю відповідатиме її опису. При цьому відпадає необхідність у верифікації моделі на відміну технології MODEL CHECKING, яка вимагає верифікацію. Граф отриманої моделі обробляється шляхом її послідовного обходу по всіх гілках з поверненнями у попередні стани та наступною програмною реалізацією. Послідовний обхід має виконуватись для кожної гілки моделі або до кінцевого її стану, або до стану, який вже був оброблений при обході. Обробка моделі полягає у трансляції опису моделі у внутрішнє подання для наступного перетворення у програму на цільовій процедурній мові програмування. При цьому усі дії у змістовних частинах предикатів, а також умови розгалужень у процесі трансляції перетворюються у внутрішнє подання програми. Дана технологія забезпечує пряме перетворення опису моделі програми у саму програму.