Описывается комплексное использование методов формального проектирования для обеспечения синтаксической и семантической целостности компонентной модели архитектуры сложной информационной системы. Верификация корректности взаимодействия компонентов программного обеспечения проводится за счет проверки соответствия сигнатур функций в рамках предложенной алгебры функциональных интерфейсов. Для верификации обеспечения декларированной функциональности используется семантический анализ контрактов интерфейсов в рамках адаптированного аппарата аксиоматической системы Хоара. Приводится демонстрация подхода на npuмере верификации синтаксической корректности и семантической целостности модели архитектуры упрощенной электронной торговли. Ключевые слова: верификация, целостность, формальный метод, компонентная модель, функциональный интерфейс.
