随着计算机系统应用日益广泛,以软件为灵魂的信息基础设施已渗透关系国计民生的各个领域,在信息社会中发挥着至关重要的作用。软件技术飞速发展和功能需求不断提高使软件系统变得日趋复杂。这些系统的失败小则造成不便,大则会带来灾难性的损害乃至付出生命的代价。因此,软件的正确性、可靠性需求显得迫切而关键。而确保系统可靠性的核心就是接受系统内外环境中错误会时常发生的事实,保证系统继续提供预期的应有服务。这样的技术便是容错。研究者已开发出大量的容错机制,然而,现阶段大多的容错解决方法中只关注在执行阶段的实现而忽视了软件开发的早期阶段,特别是设计阶段。这可能造成容错需求和执行阶段处理容错之间的严重脱节。软件系统的需求通常可以分为功能性需求和非功能性需求。功能性需求描述系统预期应提供的功能或服务。非功能性需求指那些除功能以外的系统性能和系统特性的需求。现实中众多非功能性需求所涉及到的关注点往往彼此交织重叠,而且与功能性需求也存在交织现象。传统方法在实现中常常导致非功能性代码缠绕或分散于功能性代码中,给软件设计和开发带来困难,降低了效率和可维护性。面向方面技术,可以将这些非功能性需求从功能性需求中清晰地分离出来,运用“方面”来模块化横切关注点,然后以一种松耦合的方式将一个个独立的关注点编织成一个完整的系统。软件的容错性质绝大多数为非功能性需求,实现横切多个功能模块。因此用方面对容错性质进行建模和实现可大大提高软件的可扩展性、可维护性及可重用性。现阶段存在很多面向方面的建模方法,可以大致分为以对UML扩展为代表的非形式化方法和以有限自动机为代表的形式化方法两类。然而非形式化方法缺乏严格的验证,增大系统的不可靠性。而现存的形式化建模方法又复杂,且需要寻求额外的验证工具。因此一种介乎其间的方法显得尤为重要。Petri网有着严格的数学基础和丰富的验证方法及工具,能够直观、简洁地表现系统的行为,并且对系统的并发性、异步性、不确定性具有很强的分析能力,不仅有助于定性的理解系统的动态行为,还可以定量的计算各种性能指标,特别适合于系统建模。层次着色Petri网包括一系列子网,并且它们之间以形式化的方式互相关联。这些特性自然符合了容错方面的分离和独立模块化,以及后期与基本模块的合成。而模型的构造、仿真和分析均可以采用着色Petri网自身丰富的验证工具来完成。本文首先运用Petri网来分析面向方面系统的结构特性。接着运用层次着色Petri网来分析复杂的容错系统的数据特性。本文主要的创新工作如下：●提出了基于用例的面向方面的Petri网建模方法。该方法首先给出面向方面的用例建模方法,在传统的UML用例模型上扩展以支持面向方面的概念表示。用形式化的方式将用例视图转换成Petri网的形式化模型,从而支持形式化的分析来克服UML用例非形式化及半形式化的不足,及时检测出用例视图中的可能存在的需求和建模错误。●将时态逻辑引入面向方面的Petri网检验与分析中。利用时态逻辑公式检验转换后的面向方面的Petri网模型的正确性,通过分析Petri网的执行序列来检验方面织入时机的合理性。●提出了基于着色Petri网的面向方面的建模技术。充分利用了着色Petri网中的层次概念与子模块管理机制来实现方面从基本模块的分离,以及与基本模块的合并。提出AOHCPNM和形式化的编织机制。通过CPN Tools中的ASK-CTL对状态空间进行分析,将对状态的查询转化为时态公式,然后运行公式,根据得到的真假值结果达到模型验证和系统性能分析的目的。●提出面向方面的容错模型建模与分析技术。该技术基于着色Petri网的面向方面的建模技术,将基本模块与容错方面建模为独立的子模块,通过一般替代变迁与特殊替代变迁(切入点变迁)相关联。在此基础上提出异常集和异常闭包,分别对错误检测,异常处理和复执等容错策略建立相应的模型。利用CPN Tools中的状态空间和模拟器对容错模型的执行进行正确性,合理性,有效性的验证。