# Automated Analysis of Multi-View Software Architectures

## TL;DR

This paper presents a method to formally validate multi-view software architectures early in development by constructing a unified model in Promela, enabling model checking and debugging of architectural models.

## Contribution

It introduces a novel approach to fuse UML diagrams into a single formal model for early validation of multi-view architectures.

## Key findings

- Successfully implemented as a plugin for Enterprise Architect.
- Used SPIN model checker to identify corner cases in industrial models.
- Demonstrated effectiveness in debugging multi-view architectural models.

## Abstract

Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for certain stylized, and widely used, multi-view architectures by suitably interpreting and fusing sub-models from different UML diagrams. Possible counter-examples produced by model checking are fed back as test scenarios for debugging the multi-view architectural model. We have implemented this algorithm as a plug-in for the Enterprise Architect development tool, and successfully used SPIN model checking for debugging some industrial architectural multi-view models by identifying a number of undesirable corner cases.