Моделювання, верифікація та розробка програм
Анотація
У статті розглядається удосконалення методу MODEL CHECKING при створенні програм. При цьому те-
хнічне завдання у вигляді низки вимог, які записуються за допомогою рівнянь темпоральної логіки, викорис-
товуються безпосередньо для побудови автоматної моделі майбутньої програми. Таким чином, при створенні
моделі одразу здійснюється її верифікація, оскільки вимоги будуть виконуватись у процесі побудови моделі.
В подальшому автоматна модель, яка являє собою логічну структуру програми, використовується для ство-
рення програми на будь-якій процедурній мові програмування.
Посилання
Карпов Ю.Г. MODEL CHECKING. Верификация параллельных и распределенных программных си-
стем. /Ю.Г. Карпов – СПб.; БХВ-Петербург, 2010.- 560 с.
Салапатов В.І. Синтаксичний аналіз із розподілом лексем на групи / В. Салапатов// Вісник національ-
ного технічного університету України «КПІ», Інформатика, управління та обчислювальна техніка. Київ. –
- № 49. - C. 29-33.
