## 2 Related Work
### System Composition
#### 2.1.2 Logic-Based Proposals  
On the contrary, the logic-based proposals are more suitable for dynamic verification, as they can evaluate various system states and their change over time. The theoretic foundations are surveyed in [24]. From the various approaches, the model-based solutions meet the design challenges and are the most promising. A key advantage is the abstraction level that is provided for an examined application domain. Therefore, they offer a set of concepts which are customized to specific application fields. Historically, the Model Integrated Computing (MIC) [25] was designed for formal analysis, validation, verification, and development of embedded systems. It utilizes the Domain Specific Modeling Language (DSML) [26], which can be also expressed by UML meta-models, to provide the abstraction in an application domain. Such general composition proposals are presented in [27; 28; 29; 30]. The Society of Automotive Engineers (SAE) [27] standardized the Architecture Analysis and Design Language (AADL) [28] for modeling and systems' analysis. It can express the hardware/software layers of embedded systems while assuring real-time requirements, such as fault-tolerance, safety, power consumption, schedulability, etc. With AADL the underlying setting is disassembled in hardware, software, or system components. _Interface structures_ determine the externally disclosed features, such as utilized ports, while the _implementation structures_ determine the inner elements, such as the sub-components for a main component and their connections. Thereupon, several modern AADL-based solutions or other model-driven settings (e.g., [29; 30; 31; 32; 33; 34]) have been proposed. SMoLES [30] uses DSML to express in an abstract way the system's configurations and provide a concise syntax for embedded systems' implementation. System components are defined as objects which are synchronized with each other and exchange information. Components constitute the building blocks for a system, containing input/output ports to receive/send data, accordingly. An assembly is comprised of components, presenting how they are connected. Dracena [31] is an IoT data processing platform. It models the components interactive modules as plug-ins of data-processing logic and the composition as distributed stream processing in the level ofthese components and their involved plug-ins. Dracena supports pre-composition verification and has been successfully applied in the IoT applications for smart vehicles. The proposal in [32] models the interaction of IoT systems by analyzing Message Sequence Charts (MSCs) for the utilized messaging protocol. Its current version verifies the composition of systems that use the protocol Constrained Application Protocol (CoAP) [33]. Post-composition validation is performed afterwards. A packet sniffer records the communication of the network for a specified period. Then, based on the context knowledge of the messaging protocol the system creates the MSCs and based on their analysis it derives if the compositions comply with the design specifications or not. However, as the overall solution has many drawbacks when it comes on the post-composition of actual systems as it is not generic and it requires significant resources and effort. BLESS [34] constitutes a behavioral interface specification language and proof environment for AADL. The components create AADL contracts, capturing timing and functional aspects. The pre-composition verification is performed by checking the compatibility of two interfaces while post-composition validation is achieved via the related composition contracts that the incorporated components must fulfill. The IoT Composer [35] models the behavioral aspects of IoT objects and their compositions, and performs pre-composition verification that the integration can be achieved as well as post-composition validation that the integrated components are co-working properly. Compositions are defined as interface bindings.