论文部分内容阅读
随着软件产业的迅速发展，软件系统的功能和结构日益复杂，人们对于软件产品的质量要求也越来越高。最常用的程序质量问题检测的技术包括软件测试和形式化验证。两种方法各有优缺点。形式化验证可以很好证明软件行为符合某种规范，可是方法复杂，不易实施；软件测试则恰恰相反，它实施简单，可是只能保证软件行为在测试用例覆盖的情况下正常。作为两者优点的结合体，运行时验证方法应运而生。
运行时验证技术的基础是验证规约的描述。现有运行时验证技术的大多数使用时序逻辑等形式化方法描述规约，对使用人员有较高要求，造成了这项技术难以为工程师所用。近年来，统一建模语言UML已成为事实上的工业标准，得到了广泛的普及，模型驱动的体系结构的兴起也使得模型驱动的软件工程也正在逐步得到应用。本文研究了UML模型驱动的运行时验证技术，采用描述软件设计者期望的程序运行时行为的设计层次上的UML交互模型作为规约对软件进行运行时验证，主要工作如下：
(1)针对现有offline模式的基于UML交互模型的运行时验证方法存在的问题，在模型解析、程序插桩、信息映射、一致性验证方面做了改进。
(2)进一步提出了基于online模式的运行时验证方法。该方法采用UML交互模型来描述的程序运行过程中不允许出现的场景规约，并且通过基于Aspect的监控模块实时监控程序运行，当监控到程序运行行为与该不允许出现的场景一致时，自动执行恢复程序。
(3)对基于online和offline模式的验证方法，分别实现了验证工具原型：JVerifier和JMonitor，并完成了实例研究。