带价格时间自动机网络的随机语义与统计模型检验
软件工程
2014-12-01 v2
摘要
本文基于组件间的竞争，为带价格时间自动机网络(NPTA)提供了一种自然的随机语义。该语义为概率加权 CTL 性质(PWCTL)的满足奠定了基础，保守地扩展了时间自动机关于 TCTL 的经典满足概念。特别地，该扩展允许用性能性质来细化时间自动机在 TCTL 中可表达硬实时性质，例如，以时间和成本受限性质的概率保证形式。本文的第二个贡献是应用统计模型检验(SMC)，基于 NPTA 的一定数量的独立运行，以期望的置信水平高效估计非嵌套 PWCTL 模型检验问题的正确性。除了应用经典 SMC 算法，我们还提供了一种扩展，允许在参数化设置下高效比较 NPTA 的性能性质。第三个贡献是我们成果的高效工具实现及其在若干案例研究中的应用。
引用
@article{arxiv.1106.3961,
title = {Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata},
author = {Alexandre David and Kim G. Larsen and Axel Legay and Marius Mikučionis and Danny Bøgsted Poulsen and Jonas van Vliet and Zheng Wang},
journal= {arXiv preprint arXiv:1106.3961},
year = {2014}
}