Towards a Unified Informatic Model for Cognitive Buildings: Integrating BIM, Actor Models, and Dynamic Fault Trees Using Bigraphical Reactive Systems
摘要
This paper extends our previous work on the Actors@BIM framework by introducing a tower of informatic models for cognitive building by leveraging Building Information Modeling (BIM), Actor Model of computation and Dynamic Fault Trees(DFTs). We envisage that as buildings become smarter and software-intensive there will be requirements to formally capture various aspects of a cognitive building and understand and analyse them using formal methods. This paper’s primary contribution is the unification of these three models through the use of a common formal meta-modelling framework of the Bigraphical Reactive system. This will enable the different models to be merged as a coherent whole to model future Cognitive Buildings. The key contributions of the paper are as follows: (a) We provide a framework for Modelling cognitive buildings by utilizing three different models each addressing a unique concern within the cognitive building ecosystem namely: BIM for structural, design and architectural-related concerns, Actors as a model for defining the behaviour of the cyber elements like sensor, computers, actuators, and communication elements within the cognitive buildings and Dynamic Fault Trees which can capture and model safety and reliability aspects within the cognitive building. Our Modelling technique offers a significant advantage over other formalisms like Petri Nets and State Machines. By using a common meta-model of BRS to represent BIM, Actors, and DFTs, we enable interaction among these models which was previously difficult to achieve. Further, this integration allows us to utilize a unified set of tools for the formal Verification of various design concerns and aspects of cognitive buildings, streamlining the Verification process across different domains. (b) We present the formal Semantics of Dynamic Fault Trees(DFTs) using Bigraphical Reactive Systems (BRS). To the best of our knowledge, this is the first instance of BRS being employed to model DFTs. (c) We detail the software architecture and Integrated Development Environment (IDE) built around our tower of informatic models, offering Domain Specific Languages (DSLs) for each formalism within the model. This IDE facilitates formal Verification of design scenarios using tools like BigraphER and model checkers such as PRISM.