Аннотация доклада.

Использование моделей и основанных на них средств формальной верификации в качестве способа снижения количества дефектов в программном обеспечении ведется с 1970-х годов. На настоящее время одним из основных препятствий к широкому применению формальных методов верификации, является плохая масштабируемость существующих подходов. В докладе рассматривается подход к реинжинирингу существующего и разработке нового программного обеспечения с учетом требований к его верификации на базе модели λ-исчисления с использованием предметно-ориентированных языков.