自上个世纪90年代初期开始，软件体系结构受到了学术界广泛的关注与重视，并被认为将会在未来的软件开发中起到重要的作用。随着软件体系结构研究的发展，体系结构模型中对系统行为描述的支持成为一个亟待解决的问题。其中，如何在体系结构层次显式描述系统，并尽可能自动化地进行系统行为的分析和验证是体系结构研究中的一个难点。 模型检查方法的日臻成熟为解决上述问题带来了契机。模型检查是一种对系统正确性约束的自动验证方法。现今的模型检查工具已经具有了较强的对形式化系统分析与验证的能力。因此，将模型检查方法应用于软件体系结构是一条解决上述难点的可行途径。 本文的主要工作包括：(1)借用了UML顺序图的标记，提出了体系结构层次描述系统行为及约束的模型ABC/BD，并给出了其语义；(2)采用模型检查方法设计并部分实现了对ABC/BD进行分析与验证的工具ABC/ABC，并与ABCTool集成。进一步，通过状态消减算法使得ABC/ABC处理问题的范围和规模得到增加。(3)通过实例展示了ABC/ABC在基于SA的分析与验证中的应用，并通过初步的实验证实了ABC/ABC可以处理中等规模的体系结构模型。