### Abstract

The architecture of a system describes the system's overall organization into components and connections between those components. With the emergence of mobile computing, dynamic architectures have become increasingly important. In such architectures, components may appear or disappear, and connections may change over time. In the following we mechanize a theory of dynamic architectures and verify the soundness of a corresponding calculus. Therefore, we first formalize the notion of configuration traces as a model for dynamic architectures. Then, the behavior of single components is formalized in terms of behavior traces and an operator is introduced and studied to extract the behavior of a single component out of a given configuration trace. Then, behavior trace assertions are introduced as a temporal specification technique to specify behavior of components. Reasoning about component behavior in a dynamic context is formalized in terms of a calculus for dynamic architectures. Finally, the soundness of the calculus is verified by introducing an alternative interpretation for behavior trace assertions over configuration traces and proving the rules of the calculus. Since projection may lead to finite as well as infinite behavior traces, they are formalized in terms of coinductive lists. Thus, our theory is based on Lochbihler's formalization of coinductive lists. The theory may be applied to verify properties for dynamic architectures.

### License

BSD License

### History

June 7, 2018
  adding logical operators to specify configuration traces (revision 09178f08f050)

### Topics

- Computer science/System description languages

### Session DynamicArchitectures

- Configuration_Traces
- Dynamic_Architecture_Calculus

### Depends on

- Coinductive

### Used by

- A Theory of Architectural Design Patterns

## Cite

×

DynamicArchitectures-AFP

    @article{DynamicArchitectures-AFP,
      author  = {Diego Marmsoler},
      title   = {Dynamic Architectures},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/DynamicArchitectures.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jul 31, 2017 : Isabelle2016-1