Рассмотрены варианты использования формальных моделей для описания поведения распределенных приложений, функционирующих в распределенной сетевой среде. Особое место среди них занимают приложения реального времени, корректность которых зависит от времени, затраченного на выполнение определенных операций, например на обработку текущих координат самолета и принятие решения об изменении его курса. К числу таких относятся приложения, реализующие управление бортовыми автономными объектами или большими, сложно организованными системами, работоспособность которых критически важна. Вопросы контроля за состоянием подобных систем, в том числе с использованием формальных моделей, являются крайне актуальными.
