Формальная спецификация и верификация требований в архитектуре и строительстве на основе языка моделирования EXPRESS

В настоящее время цифровые технологии моделирования зданий, сооружений и инфраструктуры успешно применяются в международной и российской практике реализации сложных строительных проектов и масштабных программ. Вместе с тем, реализуемый во многих странах переход к машиночитаемым стандартам с целью повышения качества проектной документации и автоматизации ее проверки сталкивается с серьезными методологическими и инструментальными проблемами. Прежде всего они связаны со сложностью самих цифровых моделей, а также с разнообразием требований, формулируемых на естественных языках и предъявляемых к моделям на государственном, региональном, ведомственном и корпоративном уровне. Предпринимаемые попытки создания реестров требований и программных инструментов для их ведения и использования, как правило, носят специализированный характер и не обеспечивают необходимую полноту, нормализацию, согласованность, взаимосвязанность, однозначность, прослеживаемость и проверяемость описаний требований. Конструктивным, в связи с этим, представляется применение формальных методов спецификации и верификации требований, зарекомендовавших себя в системной и программной инженерии. В работе проводится сравнительный анализ программных инструментов для автоматизированной проверки нормативных требований в области строительства. Отмечается возросшая популярность инструментов, ориентированных на международные стандарты IFC (Industry Foundation Classes), IDS (Information Delivery Specification) и обеспечивающих контроль полноты объектного и атрибутного состава моделей, а также уточнение допустимых областей значений. Вместе с тем, стандарт IDS не формализован и не предусматривает задание требований, выражаемых произвольными алгебраическими условиями. Перспективным для формальной спецификации и верификации требований к цифровым моделям в строительстве представляется применение языка моделирования объектно-ориентированных данных EXPRESS, на котором специфицирована и информационная схема IFC. В качестве обоснования показывается представимость IDS спецификаций логическими выражениями и функциями EXPRESS, а также возможность задания произвольных алгебраических условий в виде декларативных правил языка EXPRESS. В качестве иллюстраций предлагаемого подхода приводятся примеры формализации строительных нормативов и сводов правил РФ, предъявляемых к безопасности зданий, сооружений и процессов. Также обсуждаются возможности гармонизации предлагаемого формального подхода со стандартом IDS в результате определения новых паттернов для представления локальных, уникальных и глобальных правил языка EXPRESS.