Structure analysis for dynamic software architecture based on spatial logic

The requirement for modifying system structure during system execution is specified by dynamic software architectures. The system architecture style should remain one style or transform within a scope so that some constraints need to be imposed on during the system execution. Our work expands such an idea along two directions in the setting of formalism. The first direction is to model the system by a graph-based calculus stressing the structure. The other direction lies in that we tailor spatial logic to be a suitable logic as the system specification for structure. The model and specification are basis for the model checking algorithm that is to verify whether the system evolution satisfies some structure constraints. We invite a master-slave architecture style as a running example from the beginning and throughout the paper to demonstrate our approach. Such work can be seen as the basis of the structure analysis for architectures.