Email Gateway (Aug 22 2022 at 15:49): Email Gateway (Aug 22 2022 at 15:49):From: Tobias Nipkow <nipkow@in.tum.de>
Dynamic Architectures
Diego Marmsoler
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.
https://www.isa-afp.org/entries/DynamicArchitectures.shtml
smime.p7s
Last updated: Apr 26 2024 at 16:20 UTC