# APML: An Architecture Proof Modeling Language

## TL;DR

APML is a new modeling language designed to help architects verify component interactions in software systems by sketching proofs at the architectural level, bridging the gap between architecture design and formal verification.

## Contribution

The paper introduces APML, a language that enables architectural proof sketching with soundness and completeness, and maps proofs to Isabelle for formal verification.

## Key findings

- APML is sound and complete for architecture contract verification.
- The language can be mapped to Isabelle for formal proof checking.
- Implementation demonstrates practical applicability with a case study.

## Abstract

To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former is done using Model Checking, while this does not seem to be the case in general the latter is done using interactive theorem proving (ITP). As of today, however, architects are usually not trained in using a full-fledged interactive theorem prover. Thus, to bridge the gap between ITP and the architecture domain, we developed APML: an architecture proof modeling language. APML allows one to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. With this paper, we introduce APML: We describe the language, show its soundness and completeness for the verification of architecture contracts, and provide an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover Isabelle. Moreover, we describe its implementation in terms of an Eclipse/EMF modeling application, demonstrate it by means of a running example, and evaluate it in terms of a larger case study. Although our results are promising, the case study also reveals some limitations, which lead to new directions for future work.