• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Software engineering for self-adaptive systems III >MCaaS: Model Checking in the Cloud for Assurances of Adaptive Systems
【24h】

MCaaS: Model Checking in the Cloud for Assurances of Adaptive Systems

机译：MCaaS：为确保自适应系统而在云中进行模型检查

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

摘要

Due to the uncertainty of what actual adaptations will be performed at run time, verifying adaptive systems at design time may lead to limited results or may even be infeasible. Run-time verification techniques have been proposed to cope with this uncertainty. Recently, there has been an increasing interest to use model checking (an important verification technique) at run time in order to verify the expected properties of adaptive systems. Given a system specification and expected system properties, a model checker determines whether or not the specification satisfies its properties in the presence of self-adaptation. One key concern is the generally high resource needs of model checking, which may prohibit its use on resource- and power-constrained devices, such as smart-phones or Internet-of-Things devices. To address this challenge, we introduce a cloud-based framework that delivers model checking as a service (MCaaS). MCaaS offloads computationally intensive model checking tasks to the cloud, thereby offering verification capabilities on demand. Adaptive systems running on any kind of connected device may take the advantages of model checking at run time by invoking the MCaaS service. To dynamically allocate the required cloud resources (CPU and memory), we employ machine learning to estimate the resource usage of an actual model checking task at run time. As proof of concept, we implement and validate the approach for the case of probabilistic model checking, which facilitates verifying typical properties such as reliability.
机译：由于不确定在运行时将执行哪些实际调整，因此在设计时验证自适应系统可能会导致结果有限或什至不可行。已经提出了运行时验证技术来应对这种不确定性。最近，人们越来越有兴趣在运行时使用模型检查（一种重要的验证技术）来验证自适应系统的预期特性。给定系统规范和预期的系统属性，模型检查器将确定在存在自适应的情况下规范是否满足其属性。一个主要关注点是模型检查通常需要大量资源，这可能会禁止模型检查在资源和功率受限的设备（例如智能电话或物联网设备）上使用。为了应对这一挑战，我们引入了一个基于云的框架，该框架提供了模型检查即服务（MCaaS）。 MCaaS将计算量大的模型检查任务卸载到云中，从而按需提供验证功能。在任何类型的已连接设备上运行的自适应系统都可以通过调用MCaaS服务在运行时利用模型检查的优势。为了动态分配所需的云资源（CPU和内存），我们使用机器学习来估计运行时实际模型检查任务的资源使用情况。作为概念验证，我们在概率模型检查的情况下实现并验证该方法，这有助于验证诸如可靠性之类的典型属性。

著录项

  • 来源
  • 会议地点 Dagstuhl Castle(DE)
  • 作者

    Amir Molzam Sharifloo; Andreas Metzger;

  • 作者单位

    paluno (The Ruhr Institute for Software Technology), University of Duisburg-Essen, Essen, Germany;

    paluno (The Ruhr Institute for Software Technology), University of Duisburg-Essen, Essen, Germany;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号