1. Наука
  2. Видання
  3. Системи обробки інформації
  4. 1(108)'2013
  5. МЕТОД ФОРМАЛЬНОЇ ВЕРИФІКАЦІЇ UMC: UML MODEL CHECKING

МЕТОД ФОРМАЛЬНОЇ ВЕРИФІКАЦІЇ UMC: UML MODEL CHECKING

Є.І. Політько, О.М. Тарасюк, А.В. Горбенко
Анотації на мовах:

У статті аналізуються існуючі проблеми інженерії програмного забезпечення, обумовлені складністю сучасних програм і паралельністю виконання взаємодіючих процесів. Виконано огляд формальних методів розробки і верифікації, що дозволяють довести відповідність моделей програм і систем формальним вимогам. Розглянуто особливості методу формальної верифікації Model Checking і його розвиток для верифікації діаграм станів UML. Розглянуто синтаксис і семантику темпоральної логіки μUCTL і формальне подання моделей UML у вигляді системи переходу з подвійною позначкою L2TS.
Ключові слова: програмування, формальні методи, верифікація, Model Checking, UML