| Аннотацiя: | В статье анализируются существующие проблемы инженерии программного обеспечения, обусловленные сложностью современных программ и параллельностью выполнения взаимодействующих процессов. Выполнен обзор формальных методов разработки и верификации, позволяющих доказать соответствие моделей программ и систем формальным требованиям. Рассмотрены особенности мептода формальной верификации Model Checking и его развтие для верификации диаграмм состояний UML. |