Formal specification and verification of requirements in architecture and construction using the EXPRESS modeling language

Cover Page

Cite item

Full Text

Open Access Open Access
Restricted Access Access granted
Restricted Access Subscription Access

Abstract

Currently, digital technologies for modeling buildings and infrastructure are successfully used in international and national practice in the implementation of complex construction projects and large-scale programmes. At the same time, the transition to machine-readable standards being implemented in many countries in order to improve the quality of design documentation and to automate its verification faces serious methodological and technical problems. First of all, they are associated with the complexity of the digital models, as well as with the variety of requirements formulated in natural languages and imposed on models at the state, regional, departmental and corporate levels. Attempts to create catalogues of requirements and software tools for their maintenance and use, usually have specialized nature and do not provide the necessary completeness, normalization, consistency, linked set, unambiguity, traceability and validatability of requirement descriptions. In this regard, it seems constructive to use formal methods for specification and verification of requirements that have proven themselves in system and software engineering. The paper provides a comparative analysis of software tools for automated verification of regulatory requirements in the construction domain. There is an increased popularity of tools focused on the international standards IFC (Industry Foundation Classes), IDS (Information Delivery Specification) and providing control of the completeness of the object and attribute composition of models, as well as clarification of acceptable ranges of values. At the same time, the IDS standard is not formalized and does not provide for specifying the requirements expressed by arbitrary algebraic conditions. The use of the object-oriented data modeling language EXPRESS, in which the IFC information schema is also specified, looks promising for the formal specification and verification of requirements for digital models in construction. As a justification, it is shown that IDS specifications can be represented by logical expressions and EXPRESS functions, as well as arbitrary algebraic conditions can be specified as EXPRESS declarative rules. Examples of the formalization of some requirements from national construction standards and set of rules on the safety of buildings, structures and processes are provided in the paper as illustrations of the proposed approach. The possibilities of harmonizing the proposed formal approach with the IDS standard as a result of defining new facets for representing EXPRESS local, unique and global rules are also discussed.

Full Text

Restricted Access

About the authors

V. A. Semenov

Ivannikov Institute for System Programming, RAS

Author for correspondence.
Email: sem@ispras.ru
Russian Federation, 25, Alexander Solzhenitsyn str., Moscow, 109004

S. V. Morozov

Ivannikov Institute for System Programming, RAS

Email: serg@ispras.ru
Russian Federation, 25, Alexander Solzhenitsyn str., Moscow, 109004

S. V. Arishin

Ivannikov Institute for System Programming, RAS

Email: arishin@ispras.ru
Russian Federation, 25, Alexander Solzhenitsyn str., Moscow, 109004

O. N. Kuzina

National Research University Moscow State University of Civil Engineering

Email: kuzinaon@mgsu.ru
Russian Federation, 26, Yaroslavskoye shosse, Moscow, 129337

V. I. Rimshin

National Research University Moscow State University of Civil Engineering

Email: RimshinVI@mgsu.ru
Russian Federation, 26, Yaroslavskoye shosse, Moscow, 129337

E. V. Makisha

National Research University Moscow State University of Civil Engineering

Email: makishaev@mgsu.ru
Russian Federation, 26, Yaroslavskoye shosse, Moscow, 129337

References

  1. About buildingSMART International. https://www.buildingsmart.org/about, 22.04.2024.
  2. ISO 16739-1:2018. Industry Foundation Classes (IFC) for data sharing in the construction and facility management industries – Part 1: Data schema. Edition 1. 1474 p.
  3. ISO 29481–1:2016. Building information models – Information delivery manual – Part 1: Methodology and format. Edition 2. 29 p.
  4. BIM Collaboration Format (BCF) – buildingSMART Technical. https://technical.buildingsmart.org/standards/bcf, 22.04.2024.
  5. buildingSMART Data Dictionary (bSDD) – buildingSMART Technical. https://technical.buildingsmart.org/services/bsdd, 22.04.2024.
  6. Eichler C.C., Schranz Ch., Krischmann T., Urban H., Hopferwieser M., Fischer S. BIMcert Handbook – Basic knowledge openBIM. Edition 2024. Mironde-Verlag, Niederfrohna. 2024. 224 p. https://doi.org/10.34726/5383.
  7. Nisbet N. Using uncertainty to link compliance and creativity. ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction: Proceedings of the 13th European Conference on Product & Process Modelling. 2021. CRC Press, London. P. 29–34. https://doi.org/10.1201/9781003191476-4.
  8. ISO/IEC/IEEE29148:2018. Systems and software engineering – Life cycle processes – Requirements engineering. Edition 2. 92 p.
  9. Hull E., Jackson K., Dick J. Requirements Engineering, Third Edition. Springer-Verlag, London. 2011. 207 p.
  10. Kuliamin V.V. Integration of verification methods for program systems-. Programming and Computer Software. 2009. V. 35. № 4. P. 212–222. https://doi.org/10.1134/S0361768809040057.
  11. ISO/IEC19505-1:2012. Information technology – Object Management Group Unified Modeling Language (OMG UML) – Part 1: Infrastructure. Edition 1. 220 p.
  12. ISO/IEC19507:2012. Information technology – Object Management Group Object Constraint Language (OMG OCL). Edition 1. 233 p.
  13. ISO 10303-11:2004. Industrial automation systems and integration – Product data representation and exchange – Part 11: Description methods: The EXPRESS language reference manual. Edition 2. 255 p.
  14. EXPRESS Data Manager™ – Jotne Connect. https://jotneit.com/products/express-data-manager, 22.04.2024.
  15. Soliman-Junior J., Tzortzopoulos P., Baldauf J.P., Pedo B., Kagioglou M., Formoso C.T., Humphreys J. Automated compliance checking in healthcare building design. Automation in Construction. 2021. V. 129. https://doi.org/10.1016/j.autcon.2021.103822.
  16. D Modeler | Open BIM Systems. https://www.openbimsystems.ru/en/7d-modeler, 22.04.2024.
  17. BIMcollab Zoom: model validation that gets issues solved. https://www.bimcollab.com/en/products/bimcollab-zoom, 22.04.2024.
  18. BlenderBIM Add-on – beautiful, detailed, and data-rich OpenBIM. https://blenderbim.org, 22.04.2024.
  19. Open IFC Viewer. https://openifcviewer.com, 22.04.2024.
  20. IFC Checker and BIM Validation | usBIM.checker | ACCA software. https://www.accasoftware.com/en/ifc-checker, 22.04.2024.
  21. Li B., Schultz C., Dimyadi J., Amor R. Defeasible reasoning for automated building code compliance checking. ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction: Proceedings of the 13th European Conference on Product & Process Modelling. 2021. CRC Press, London. P. 229–236. https://doi.org/10.1201/9781003191476-32.
  22. Information Delivery Specification IDS – buildingSMART Technical. https://technical.buildingsmart.org/projects/information-delivery-specification-ids, 22.04.2024.
  23. Natsional’naya TIM Platforma | Servis validatsii IFC modelej [National BIM Platform | IFC model validation service] (in Russian). URL: https://bim.ispras.ru/validate-ifc, accessed 22.04.2024.
  24. van Berlo L., Willems P., Pauwels P. Creating Information Delivery Specifications using linked data. Proceedings of the 36th International CIB W78 Conference. 2019. P. 647–660.
  25. Kremer N., Beetz J. Extending Information Delivery Specification for linking distributed model checking services. Proceedings of the 40th International CIB W78 Conference. 2023. https://doi.org/10.35490/EC3.2023.266.
  26. GOST R10.0.02-2019/ISO 16739-1:2018 Sistema standartov informatsionnogo modelirovaniya zdanij i sooruzhenij. Otraslevye bazovye klassy (IFC) dlya obmena i upravleniya dannymi ob ob’ektah stroitel’stva. Chast’ 1. Shema dannyh [GOST R 10.0.02-2019/ISO 16739-1:2018. System of standards for building information modeling. Industry Foundation Classes (IFC) for exchanging and managing construction site data. Part 1. Data schema]. 28 p. (in Russian).
  27. Software Implementations – buildingSMART Technical. https://technical.buildingsmart.org/resources/software-implementations, accessed 22.04.2024.
  28. ISO 16739-1:2024. Industry Foundation Classes (IFC) for data sharing in the construction and facility management industries – Part 1: Data schema. Edition 2. 496 p.
  29. ISO 10303-1:2024. Industrial automation systems and integration – Product data representation and exchange – Part 1: Overview and fundamental principles. Edition 3. 23 p.
  30. ISO 10303-21:2016. Industrial automation systems and integration – Product data representation and exchange – Part 21: Implementation methods: Clear text encoding of the exchange structure. Edition 3. 3 p.
  31. ISO 10303-28:2007. Industrial automation systems and integration – Product data representation and exchange – Part 28: Implementation methods: XML representations of EXPRESS schemas and data, using XML schemas. Edition 1. 309 p.
  32. ISO/TS10303-26:2011. Industrial automation systems – Product data representation and exchange – Part 26: Implementation methods: Binary representation of EXPRESS-driven data. Edition 1. 5 p.
  33. Staab S., Studer R. (eds.) Handbook on Ontologies, Second Edition. Springer-Verlag, Berlin. 2009. 811 p.
  34. IFC Implementation Guidance – buildingSMART Technical. https://technical.buildingsmart.org/resources/ifcimplementationguidance, accessed 22.04.2024.
  35. van Berlo L.A.H.M., Beetz J., Bos P., Hendriks H., van Tongeren R.C.J. Collaborative engineering with IFC: New insights and technology. ECPPM 2012 – eWork and eBusiness in Architecture, Engineering and Construction: Proceedings of the 9th European Conference on Product & Process Modelling. 2012. CRC Press, London. P. 811–818.
  36. Borrmann A., Beetz J., Koch C., Liebich T., Muhic S. Industry Foundation Classes – A standardized data model for the vendor-neutral exchange of digital building models. Building Information Modeling – Technology Foundations and Industry Practice. Springer, Cham. 2018. P. 81–126. https://doi.org/10.1007/978-3-319-92862-3_5
  37. van Berlo L., Krijnen T.F., Tauscher H., Liebich T., van Kranenburg A., Paasiala P. Future of the Industry Foundation Classes: towards IFC5. Proceedings of the 38th International CIB W78 Conference. 2021. P. 123–137.
  38. UniFormat® – Construction Specifications Institute. https://www.csiresources.org/standards/uniformat, accessed 22.04.2024.
  39. OmniClass® – Construction Specifications Institute. https://www.csiresources.org/standards/omniclass, accessed 22.04.2024.
  40. Klassifikator Stroitel’noj Informatsii [Construction Information Classifier] (in Russian). http://ksi.faufcc.ru, accessed 22.04.2024.
  41. Tomczak A., Benghi C., van Berlo L., Hjelseth E. Requiring Circularity Data in BIM with Information Delivery Specification. Journal of Circular Economy. 2024. V. 1. № 2. P. 1–13. https://doi.org/10.55845/REJY5239
  42. IDS – Machine readable Information Delivery Specification. URL: https://github.com/buildingSMART/IDS/blob/master/Documentation, accessed 22.04.2024.
  43. BIM Collaboration Format v3.0 Technical Documentation. https://github.com/buildingSMART/BCF-XML/tree/release_3_0/Documentation, accessed 22.04.2024.
  44. Semenov V., Ilyin D., Morozov S., Tarlapan O. Effective consistency management for large-scale product data // Journal of Industrial Information Integration. 2019. V. 13. P. 13–21. https://doi.org/10.1016/j.jii.2018.11.006.
  45. Morozov S.V., Ilyin D.V., Semenov V.A., Tarlapan O.A. Biblioteka ogranichenij dlya spetsifikatsii industrial’nyh modelej dannyh [A constraint library for specification of industrial data models]. 2015. V. 27. N. 4. P. 69–110 (in Russian). https://doi.org/10.15514/ISPRAS-2015–27(4)-5.
  46. Semenov V.A., Arishin S.V., Semenov G.V. Formal rules to produce object notation for EXPRESS schema-driven data. Programming and Computer Software. 2022. V. 48. № 7. P. 455–468. https://doi.org/10.1134/S0361768822070076.
  47. Svod pravil SP 60.13330.2020. Otoplenie, ventilyatsiya i konditsionirovanie vozduha [Set of rules SP 60.13330.2020. Heating, ventilation and air conditioning]. 149 p. (in Russian).
  48. Svod pravil SP 1.13130.2020. Sistemy protivopozharnoj zashchity. Evakuatsionnye puti i vyhody. [Set of rules SP 1.13130.2020. Fire protection systems. Evacuation routes and exits]. 46 p. (in Russian).
  49. GOST 475-2016. Bloki dvernye derevyannye i kombinirovannye. Obshchie tehnicheskie usloviya [GOST 475–2016. Wooden and combined door blocks. General technical conditions]. 35 p (in Russian).
  50. Trebovaniya k tsifrovym informatsionnym modelyam ob’ektov kapital’nogo stroitel’stva, predstavlyaemym dlya provedeniya ekspertizy. Redaktsiya 3.0 (TGE.TIM-3.0) [Requirements for digital information models of capital construction projects submitted for expertise. Edition 3.0 (TGE.TIM-3.0)]. SPb GAU “Tsentr Gosudarstvennoj Ekspertizy” [SPb SAI “Center for State Expertise”]. 2022. 203 p (in Russian).

Supplementary files

Supplementary Files
Action
1. JATS XML
Download
2. Fig. 1. The process of requirements verification in construction based on open standards.

Download (37KB)
Indexing metadata
3. Fig. 2. An example of an object specification with a local rule in the EXPRESS language.

Download (220KB)
Indexing metadata
4. Fig. 3. EXPRESS language function for determining the presence of aggregation relations.

Download (134KB)
Indexing metadata
5. Fig. 4. EXPRESS language functions for searching for assigned properties.

Download (451KB)
Indexing metadata
6. Fig. 5. Function in the EXPRESS language for comparing the classification systems used.

Download (214KB)
Indexing metadata
7. Fig. 6. EXPRESS language function for matching materials by name or category.

Download (227KB)
Indexing metadata
8. Fig. 7. Formalization of the requirement for the permissible aspect ratio of air ducts in the form of a local rule in the EXPRESS language.

Download (235KB)
Indexing metadata
9. Fig. 8. Formalization of the requirement for the number of evacuation exits from a building in the form of a global rule in the EXPRESS language.

Download (225KB)
Indexing metadata
10. Fig. 9. Formalization of the requirement for uniqueness of room numbers in the form of a uniqueness rule in the EXPRESS language.

Download (189KB)
Indexing metadata
11. Fig. 10. Formalization of the requirement for the absence of geometric collisions between walls in the EXPRESS language.

Download (98KB)
Indexing metadata
12. Fig. 11. Screenshot of the main window of the Perspective Requirements Editor.

Download (116KB)
Indexing metadata
13. Fig. 12. Screenshot of the Requirements Specification Editor window.

Download (150KB)
Indexing metadata

Copyright (c) 2024 Russian Academy of Sciences