Formal Specification and Verification of Requirements in Architecture and Construction using the EXPRESS Modeling Language

Currently, digital technologies for modeling buildings and infrastructure are successfully used in international and national practice for the implementation of complex construction projects and large-scale programmes. At the same time, the transition to machine-readable standards, implemented in many countries to improve the quality of design documentation and automate its verification, faces serious methodological and technical challenges. First of all, these challenges are due to the complexity of digital models, as well as the variety of requirements formulated in natural languages and imposed on these models at the state, regional, departmental, and corporate levels. Attempts to create catalogs of requirements and software tools for their management and use generally have specific purposes and do not provide necessary completeness, normalization, consistency, interconnectedness, unambiguity, traceability, and validability of requirements description. In this regard, it seems reasonable to use formal methods for specification and verification of requirements that have proven themselves in system and software engineering. This paper provides a comparative analysis of software tools for automated verification of regulatory requirements in the construction domain. There is a growing interest in tools focused on international standards, such as Industry Foundation Classes (IFC) and Information Delivery Specification (IDS), that allow one to control the completeness of the object and attribute composition of models, as well as the clarification of acceptable domains of values values. However, the IDS standard is not formalized and does not enable the specification of requirements expressed in terms of arbitrary algebraic conditions. The EXPRESS object-oriented data modeling language, in which the IFC data schema is specified, seems promising for the formal specification and verification of requirements for digital models used in the construction industry. As a substantiation, it is shown that IDS specifications can be represented by logical expressions and EXPRESS functions, as well as that arbitrary algebraic conditions can be specified as EXPRESS declarative rules. To illustrate the proposed approach, we consider some examples of the formalization of requirements from national construction standards and sets of rules concerning the safety of buildings, structures, and processes. The possibility of harmonizing the proposed formal approach with the IDS standard by defining new facets for the representation of local, uniqueness, and global EXPRESS rules is also discussed.