# Trusted Composition of Internet of Medical Things over Imperfect Networks
## 3 Background  
The Architecture Analysis & Design Language (AADL) is SAE International standard AS5506D, and was created for systems engineering of cyber-physical systems [27]. AADL has well-defined semantics for components and their composition. In particular, AADL component types describe everything visible from outside the component (features, ports, parameters, and accesses), while component implementations describe their internals. Each component type may have several component implementations. Component implementations may be composite components containing subcomponents and connections between them, or may be hardware and/or software not further partitioned.  
In AADL, logical architectures (software) are modeled with _process_, _data_, _subprogram_, _thread_, and _thread group_ components. Process components model the protected memory space shared among thread subcomponents, which model active software which can issue and respond dynamically to events. Data components model types, persistent values directly accessible by multiple threads. Subprogram components model procedures and functions, which must be invoked by threads or other subcomponents.  
Physical architectures, in AADL, are modeled with _processor_, _memory_, _bus_, and _device_ components. Hardware that executes software is modeled with processor components. Memory components model data storage. Device components model other physical entities like actuators and sensors or custom logic. Bus components model the physical connections (i.e., wires) between execution platform components.  
AADL also provides _system_ components to model composition of logical and physical components, and _abstract_ components to model interfaces without further elaboration. The Open Source AADL Tool Environment (OSATE) [28] is an IDE with analysis tools built on Eclipse to implement AADL for the modeling and analysis of real-time embedded systems.  
The core AADL standard only provides support for structural modeling of embedded computing systems, and nothing related to detailed behavior of the software and physical processes which are controlled by the software can be modeled. The Behavior Language for Embedded Systems with Software (BLESS) is an annex sublanguage of AADL that augments the core architecture language to define specification and behavior implementations [29]. A BLESS plugin to OSATE allows program development and transforms programs with proof outlines into deductive proofs.  
BLESS annex sublanguage uses five domain-specific languages (DSLs) edited with a plugin extension to OSATE. Each DSL is used in AADL subclauses, libraries, or properties. An _Assertion_ language to make assertions (statements of fact), a _Typedef_ language to define types and units, a _Unit_ language to specify measure units, a _State Machine_ language to express thread behavior, and an _Action_ language to express imperative control-flow computation.  
The BLESS proof assistant transforms program proof outlines into deductive proofs, given human selection of proof tactics. For more details, refer to the BLESS reference and proof assistant guide [30].  
AADL facilitates system engineering to minimize problems discovered during systems integration when they are most costly to remedy. Architecture-Centric Virtual Integration (ACVI) is a design methodology for using AADL to preclude system integration issues [31]. ACVI was adapted for use to compose interoperable medical devices as medical device virtual integration (MDVI) in [5]. With MDVI, systems engineers use AADL's property mechanism to attach assertions (predicates or expressions) to component features, expressing what is guaranteed to be true (for outputs) or assumed to be true (for inputs). Connections between features give rise to assume-guarantee contracts, which can be formally verified before the components are designed. Additionally, components may have invariants, much like loop invariants. Invariants for composite components are implied by invariants of their subcomponents.