论文部分内容阅读
UML是一种通用的可视化建模语言，用于对软件进行描述、可视化处理、构建软件系统的文档。作为UML标准的一部分，对象约束语言(Object ConstraintLanguage，OCL)用来精确地描述模型的约束条件以及相互之间的关系。OCL是一种声明式语言，也是一种形式化语言。 施加于模型之上的三种常用OCL约束是前置条件、后置条件、不变式。前置条件表示当操作被激发时输入参数和模型状态的可接受值。后置条件表明操作完成时必须满足的条件，它表示操作完成时检测该操作的结果值和模型的状态。不变式是在属性的生命期内一直保持为真的规则。为了保证程序执行过程中这些约束得以满足，需要对约束进行验证。在运行时检测约束的冲突有助于软件系统的开发，尤其是大型系统和嵌入式实时系统的开发。 本文的目标是对模型施加必要的约束，得到能检测出运行时约束冲突的代码，这就要求分别为前置条件、后置条件、不变式设计出相应的代码模式。代码模式描述了OCL约束对应的可执行的Java代码(即OCL-Java代码)如何被插入到Java程序中的方式。在程序运行时一旦检测到约束的冲突，代码模式能够抛出相应的异常。 文中利用UML建模工具为系统建立模型，并基于OCL理论为该模型施加必要的约束，从而得到精确的模型。应用建模工具的自动生成代码功能得到的模型对应的Java程序中，OCL约束只以注释形式出现，本文实现了从程序中抽取出这些OCL约束。由于OCL不是一种编程语言，其约束不能在程序中直接执行，本文使用的目标语言是Java，因此要把OCL约束转化为可直接执行的Java代码(即OCL-Java代码)。为此，本文详细阐述了OCL约束转化为OCL-Java代码的实现过程。为了能在程序运行时检测出冲突的约束，需要把OCL-Java代码插入到Java程序中，使之与Java程序一起执行，从而能有效地验证声明的约束。针对简单的代码插入方案和封装方法存在的不足，本文提出了改进的代码插入方案，分别设计了前置条件代码模式、后置条件代码模式、不变式代码模式，这三种代码模式都应用了异常处理技术从而能够捕获冲突的约束。本文充分应用了Java解析器能解析Java文件的特性，实现了把OCL-Java代码插入到Java程序中。最后，应用本文提出的OCL约束验证框架在实例模型的基础上分别对不变式、前置条件、后置条件进行了验证。