...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Supporting automated containment checking of software behavioural models using model transformations and model checking
【24h】

Supporting automated containment checking of software behavioural models using model transformations and model checking

机译：使用模型转换和模型检查来支持软件行为模型的自动包含检查

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Models are extensively used in many areas of software engineering to represent the behaviour of software systems at different levels of abstraction. Because of the involvement of different stakeholders in constructing these models and their independent evolution, inconsistencies might occur between the models. It is thus crucial to detect these inconsistencies at early phases of the software development process, and especially as soon as refined models deviate from their abstract counterparts. In this article, we introduce a containment checking approach to verify whether a certain low-level behaviour model, typically created by refining and enhancing a high-level model, still is consistent with the specification provided in its high-level counterpart. We interpret the containment checking problem as a model checking problem, which has not received special treatment in the literature so far. Because the containment checking is based on model checking, it requires both formal consistency constraints and specifications of these models. Unfortunately, creating formal consistency constraints and specifications is currently done manually, and therefore, labour-intensive and error prone. To alleviate this issue, we define and develop a fully automated transformation of behaviour models into formal specifications and properties. The generated formal specifications and properties can directly be used by existing model checkers for detecting any discrepancy between the input models and yield corresponding counterexamples. Moreover, our approach can provide the developers more informative and comprehensive feedback regarding the inconsistency issues, and therefore, help them to efficiently identify and resolve the problems. The evaluation of various scenarios from industrial case studies demonstrates that the proposed approach efficiently translates the behaviour models into formal specifications and properties. (C) 2019 Elsevier B.V. All rights reserved.
机译：模型被广泛用于软件工程的许多领域，以表示软件系统在不同抽象级别上的行为。由于不同利益相关者参与构建这些模型及其独立发展，因此模型之间可能会出现不一致之处。因此，至关重要的是在软件开发过程的早期阶段，尤其是在精炼模型偏离其抽象对应模型后，立即检测出这些不一致之处。在本文中，我们引入了一种包含检查方法，以验证通常通过改进和增强高级模型创建的某些低级行为模型是否仍与高级模型中提供的规范一致。我们将安全性检查问题解释为模型检查问题，到目前为止，在文献中尚未对此进行特殊处理。因为包含检查基于模型检查，所以它既需要形式一致性约束，又需要这些模型的规范。不幸的是，创建形式上的一致性约束和规范目前是手动完成的，因此劳动强度大且容易出错。为了缓解此问题，我们定义并开发了一种自动的行为模型转换为正式规范和属性的方法。生成的形式规范和属性可以由现有的模型检查器直接用于检测输入模型之间的任何差异并产生相应的反例。而且，我们的方法可以为开发人员提供有关不一致问题的更多信息和全面的反馈，从而帮助他们有效地识别和解决问题。对来自工业案例研究的各种场景的评估表明，所提出的方法有效地将行为模型转换为正式的规范和属性。 （C）2019 Elsevier B.V.保留所有权利。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号