应对大规模软件系统的复杂性从而提高其正确性是软件工程研究的一个重要目标。形式化方法提供了描述和分析系统的行为和特征、检验和证明系统性质的理论和方法。研究开发面向软件开发过程中关键活动的形式化方法和工具,帮助软件开发人员更好地认识理解和分析问题,控制系统的复杂性,同时提供可以提高软件系统正确性的手段,是解决软件系统复杂性和正确性问题的重要途径。　　 用例驱动的软件开发过程通过用例模型定义系统的需求规约,需求规约是随后软件开发活动的重要依据。需求规约能否对需求做出准确、完整和一致的描述,关乎最终软件的质量。基于构件的软件开发方法已成为主流的软件开发方法,现代构件系统大规模、广分布和高并发的特点使得构件系统更加复杂。如何提高现代构件系统的正确性,是基于构件的软件开发过程必须解决的关键问题。　　 本文以设计演算和CSP为基本建模理论,研究提高复杂软件系统正确性的方法。研究内容包括:构建形式化的用例分析建模框架,并利用形式框架检查用例模型的一致性;设计形式化构件行为模型,并以模型为基础,研究构件的精化方法。本文主要工作如下:　　 ·面向构建复杂系统的需求规约,设计了一种用例分析建模框架。它遵循关注点分离策略,支持用户运用多个视图对系统需求进行建模:概念类图描述了问题域中的概念和概念间的关联;用例控制类描述每个用例操作的对象和型构;序列图和状态图分别以序列和控制状态转换的方式描述用例与环境进行交互的场景;功能规约函数定义了操作的功能规约;系统不变式刻画目标领域的业务规则和相关约束。　　 ·为精确地描述需求规约,并支持对需求规约进行严格地分析和验证,提出了用例分析建模框架的一种形式化描述途径。该途径基于设计演算理论,给出了用例分析建模框架中类图、用例序列图、用例状态图、功能规约函数和不变式的形式化定义。它允许将用例序列图、用例状态图和功能函数分别描述的规约进行集成,并支持利用设计演算理论对规约展开分析和验证。　　 ·针对用例分析建模框架中多个视图之间的一致性问题,给出了一种检验方法。其中,静态一致性问题把类图作为用例模型的类型系统,检查各视图中对类、类关联、类方法和类属性的使用是否与类图中的类型定义有冲突。动态一致性问题检查同一用例各个视图分别描述的功能和动态行为规约是否有冲突。　　 ·针对如何精确地刻画构件行为这一构件技术研究的重要问题,提出了一种主动构件行为的建模方法。在接口层构造基于状态的模型(契约)来描述接口的行为。同时,定义基于方法调用事件和返回事件的模型描述契约的交互行为。给出了从状态模型(契约)推导交互行为模型的方法。利用此模型,分析了主动构件内部主动行为引起的接口行为的非确定性,给出分析契约一致性的演算方法。在构件层将构件的语义定义为从其需求接口的契约到其服务接口的契约的函数。研究了从构件代码和需求接口的契约计算构件服务接口契约的方法。　　 ·针对构件系统的正确性问题,研究由构造过程提高系统正确性的构件精化方法。在接口层,以契约交互行为模型上发散、失败集合之间的包含关系定义契约的精化关系,证明了相关定理以支持应用仿真技术判定契约之间的精化关系。在构件层,以契约之间的精化关系定义构件之间的精化关系,从而可以利用契约之间的精化关系证明构件之间的精化关系。　　 ·为在构件系统自底向上的构造过程中应用精化方法,研究了构件形式模型的组装方法。构件的组装过程将一个构件需求接口中的方法与另一构件服务接口中对应的方法相连接。运行时刻,构件双方需在相连接方法的调用事件和返回事件上做两次同步。给出了计算组合后复合构件语义的方法,其中构件内部主动活动的规约直接通过非确定选择算子加以组合。　　 ·给出一个分析CORBA系统体系结构的实例,展示构件精化与组合方法在基于构件的软件开发过程中的一种应用。首先,将整个CORBA系统作为一个构件,构造其形式模型;随后分析CORBA构件域变量之间的关系,对域变量进行精化。最后对精化后的CORBA构件做分解,整个CORBA构件被分解成为一组构件的组合。运用构件的精化定理和组合定理,保证上述精化和分解结果的正确性。给出了构件精化与组合方法支撑工具的设计。