基于服务应用的定量属性离线轨迹检查
软件工程
2014-09-17 v1
摘要
基于服务的应用通常开发为合作伙伴服务的组合。服务集成商需要精确的方法来指定每个合作伙伴服务预期的质量属性，以及有效的技术来验证这些属性。在之前的工作中，我们确定了与提供基于服务的应用相关的最常见规范模式，并开发了一种支持它们的表达性规范语言 (SOLOIST)。SOLOIST 是度量时序逻辑的扩展，具有聚合时序模态，可用于编写定量时序属性。在本文中，我们解决了针对用 SOLOIST 编写的定量需求规范对服务执行轨迹进行离线检查的问题。我们提出了将 SOLOIST 转换为 CLTLB(D)（线性时序逻辑的一种变体）的方法，并将 SOLOIST 的轨迹检查归约为 CLTLB(D) 的有界可满足性检查，后者由基于 SMT 的验证工具包 ZOT 支持。我们详细介绍了将所提出的离线轨迹检查过程应用于不同类型轨迹的结果，并将其性能与之前的工作进行了比较。
引用
@article{arxiv.1409.4653,
title = {Offline Trace Checking of Quantitative Properties of Service-Based Applications},
author = {Domenico Bianculli and Carlo Ghezzi and Srdan Krstic and Pierluigi San Pietro},
journal= {arXiv preprint arXiv:1409.4653},
year = {2014}
}
备注
19 pages, 7 figures, Extended version of the SOCA 2014 paper