摘要: 简介与动机
软构件的引入之后，其应用局限于组建整体系统，但目前已扩展至其他应用领域，构件的错误将是不可接受的。对于那些容易对人的生命造成威胁、引发重大财产损失的软件，需要引入容错能力，使其在出错时仍能执行或者部分地执行预期的操作。在现存的一些建立容错系统的技术中，异常处理是使软件系统从错误中恢复的一种广为人知的机制7。异常处理在大型软件开发中的使用8，以及其在一些现代面相对象语言——例如Java, Ada, C#和C++——中的实现，在一些构件模型——例如CCM, EJB, Ice和.NET——中的实现，证明了它在当前软件开发实践中的重要性。另一方面，如果我们考虑到这样一个事实：系统代码中的很大一部分是错误的检测和处理7, 8，那就会接受异常处理机制也有其不足的事实。
为应对异常处理机制中固有的复杂性，通常要求异常行为被尽可能早地、系统化地集成到软件的开发过程中，尤其是在需求工程和体系结构设计中9。体系结构层面的容错受到了大量的关注，尤其是在错误处理方面，特别是体系结构重配置相关的问题，包括：替换、增加、去除体系结构元素或者改变配置的拓扑结构2。错误的传播及处理则不是如此。为鉴别和去除系统异常行为相关的错误，需要在体系结构的设计和实现中采用一些验证和测试技术。利用体系结构层面异常行为的验证的工作几乎没有。例如，Castor等人提出了一种用Alloy规约语言在软件体系结构上规约和验证异常控制流的解决方法6。然而，这种方法不能在验证过程中规约异常处理器的行为。另外，若验证过程中必须处理多种类型的异常时，这种方法的可扩展性不够好6。
在验证软件体系结构之前，需要用形式化的符号对其进行规约。体系结构描述语言（Architecture Description Language, ADLs）是表示体系结构的专用语言。尽管这种语言通常被认为是直观的，但是它在表示系统的某些特定方面缺乏支持。这种局限性的例子包括：异常类型、包含体系结构元素的异常控制流、异常处理场景以及产生基于模型的测试用例的操作签名等方面的表示。为克服这些局限性，需要使用一种形式化的符号来表示不同的异常类型。另外，为了表示异常控制流中的链接、变换和屏蔽，形式化的符号必须提供对含有体系结构元素的场景的规约。
在本文中，我们为开发容错的软件系统提出了一种严格的体系结构的方案。该方案基于体系结构抽象，对容错软件体系结构进行规约，并提供了验证和测试方面的支持，着眼于提高系统的可靠性。基于体系结构抽象，可以使用stereotyped UML2.0来描述容错体系结构，这又可以作为自动生成软件体系结构形式化规约的基础。在这种形式化模型上，可以对错误处理属性做形式化验证，也能自动生成测试用例来评估最终系统的正确性。在形式化规约中，我们结合了B-Method和CSP来描述软件体系结构的结构和行为。用模型检验的方法来验证软件体系结构的容错属性，尤其是异常的发出、传播和处理。最后，通过生成单元和集成测试用例来评估软件体系结构的实现。
所提方案概述
理想化容错体系结构元素
理想化容错体系结构元素（idealised fault-tolerant architectural element, iFTE）是结构化容错系统的体系结构抽象。这种抽象加强了与理想化容错构件1相关联的原则，以结构化的方法集成了错误的检测、传播和处理机制。iFTE抽象为两类行为提供了显式的分离：(1) 正常行为，即应用所提供的服务；(2) 异常行为，即错误的检测、传播和处理。为了做这种分析，iFTE提供了四类接口，如图1所示。I_iFTE_PN和I_iFTE_RN负责正常行为，I_iFTE_PA和I_iFTE_RA负责异常服务。

Figure 1: iFTE 抽象
一种严格的开发和测试方法
在我们的方法中，认为软件体系结构是第一层的单元，指导从规约到实现的应用开发。图2是所提出的开发容错软件体系结构的概述。Activity 1规约了软件体系结构，可以通过CASE工具以图形化的方式来做。在异常场景的用例中，需要规约UML构件图和UML顺序图，前者表示软件体系结构的结构，后者表示异常控制流的体系结构场景和处理器。为了生成体系结构场景，需要系统中体系结构的配置来精化用例场景。Activity 2形式化规约了软件体系结构（体系结构的配置和场景）。这个活动由一个从UML(XMI文件)到B-Method和CSP的模型自动转换过程组成。利用从UML模型中抽取结构和行为的规约来实例化形式化模板是该转化过程的工作。模板是解决方案的一部分，并且也在他人的工作中出现4, 3。Activity 3是软件体系结构的形式化验证，目的是标识异常控制流和处理器相关的设计错误。Activity 4生成测试用例和系统源代码，本文中不再给出细节。Figure 2中的整个处理过程是递归的，因为它既能够在整个系统上执行，又能够在体系结构元素的内部结构上执行。

Figure 2: 开发异常行为的过程
结论
我们为开发容错软件系统提出了一种以体系结构为中心的解决方案。使用体系结构抽象来去掉系统的细节，同时提供了分析错误的传播、检测和处理的方法。可以使用stereotyped UML 2.0来描述容错软件体系结构，这也可以作为自动生成软件体系结构形式化规约的基础。形式化模型（本文中未给出）允许形式化验证错误处理属性以及自动生成评估容错软件体系结构的测试用例。我们利用采矿系统作为案例来评估我们的方案。该案例的主要目的有三：第一个目的是评估在验证和测试软件体系结构中的异常控制流和处理的场景时，所提方法的可行性。第二个目的是为了评估所提方法是否有助于查找其他方法无法找到的错误。最后一个目的是评估软件体系结构的使用是否能够提高可理解性。
本文中的新贡献包括：(i) 基于体系结构抽象的异常处理的规约和验证；(2) 提出了一个新的规约异常控制流和处理器的形式化框架，该框架在其他不同的应用中也可以复用。
本文所提方案的局限性在于其假设体系结构元素之间的交互符合一种call-return协议。尽管这种假设简化了软件体系结构的规约，但是缺少并发性，而这在很多应用中是很关键的。为了克服这种局限，当前在研究如何修改我们的方案，使之支持基于事件的软件体系结构的规约。这样，新的形式化框架就能够处理并发的异常并协同并发构件执行的场景。