Skip to main content
U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

Well-being as a Composite Capability in the Smart Building Domain: A Formal and Technical Study



Khalid Halba, Asmaa Hailane, ahmed lbath, Edward Griffor, Anton Dahbura


Smart building value-added capabilities are gaining significant attention from various stakeholders, including the general public, researchers, and industry. One such capability is well-being, a composition of multiple atomic capabilities that characterize a smart building. Atomic functions that compose a well-being capability include temperature, noise level, pollution level, and humidity, to name a few. Multiple efforts tackled this specific capability and its composition requirements and techniques from standardization, technical, and quality of service aspects. One such effort is the IoT and CPS Composition Framework (ICCF), a novel framework for rapid modeling, specifying, verifying, and prototyping IoT and CPS capabilities. ICCF relies on the NIST CPS Framework guidelines to address different stakeholders' concerns; It also leverages composition semantics inspired by the mPlane platform to describe entities and interactions intuitively. In addition, It uses TLA+ formal verification techniques to verify the correctness of core functions. In this work, we start from the ICCF framework we published to provide the following contributions: i) describe a stakeholder-defined well-being composition capability based on the ICCF framework foundations, ii) provide an in-depth definition and characterization of the well-being capability, iii) study the formal aspects of the well-being capability, including verifying its correctness, deadlock, and state-space, iv) implement the composite capability using a lightweight microservices environment, v) and discuss results based on the different domains of interest including residential buildings and factories. Finally, we summarize this effort by discussing challenges to capabilities composition and providing paths for improvement in future work.
Proceedings Title
Building Bridges Towards Responsible Smart Cities
Conference Dates
March 9-11, 2022
Conference Location
Bilbao, Biscay, ES
Conference Title
2022 IEEE European Technology and Engineering Management Summit (IEEE E-TEMS 2022)


IoT, CPS, Composition, Smart Buildings, Well-being, Formal Verification, Micro-services


Halba, K. , Hailane, A. , Lbath, A. , Griffor, E. and DAHBURA, A. (2022), Well-being as a Composite Capability in the Smart Building Domain: A Formal and Technical Study, Building Bridges Towards Responsible Smart Cities, Bilbao, Biscay, ES, [online],, (Accessed June 14, 2024)


If you have any questions about this publication or are having problems accessing it, please contact

Created November 22, 2022, Updated January 17, 2024