中文摘要：

在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断扩大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,以更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,对传统基于模型的测试方法的一致性检验进行了扩展,实现了一致性检验框架Pro Miner,通过抽取表达模型与代码的不一致的系统性质来自动定位模型中与实际运行系统不匹配的部分,并将其表示为可直接用于模型检测的线性时序逻辑（LTL）表达式,以支持软件模型和代码间双向的一致性检验.实验结果表明,Pro Miner可有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性,而且大大减少了人力开销.

英文摘要：

Model-Driven development is currently a highly regarded software development paradigm among software developers and researchers, and model-based testing techniques are usually applied during the development to ensure the quality of software systems. With the growing size and complexity of software systems, maintaining the consistency between software models and their implementation become more and more challenging. While traditional model-based testing focuses on ensuring the software implementation comply with its designed model, this work addresses particularly the situation where the implementation is modified while software models are left outdated due to workarounds or other unexpected changes during development. The paper presents an automated consistency checking framework, Pro Miner, which extends traditional model-based testing with mining software properties that represent the identified inconsistencies as linear temporal logic（LTL）. Experiments show that this extended consistency checking technique effectively helps software designer to narrow down the specific locations of software models that need to be updated with respects to its running implementation.