Estimating latency and concurrency of asynchronous real-time interactive systems using model checking
Estimating latency and concurrency of asynchronous real-time interactive systems using model checking
复制标题
使用模型检查估计异步实时交互系统的延迟和并发性
DOI：
10.1109/vr.2016.7504688
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
H. Tramberend
中科院分区：
文献类型：
--
作者：
Stephan Rehfeld;Marc Erich Latoschik;H. Tramberend
本文介绍了模型检查作为估计异步实时交互系统 (RIS) 延迟和并行性的替代方法。并发虚拟现实 (VR) 和计算机游戏系统中常见的五种典型并发和同步方案被确定为用例。这些用例指导开发 a) 基于异步 RIS 架构的用例实现所需的软件原语，以及 b) 图形编辑器，用于基于这些原语的各种并发和同步方案（包括用例）的规范。根据 RIS 领域的典型要求评估了几种模型检查工具。因此，正式模型检查语言 Rebeca 及其模型检查器 RMC 被应用于用例规范，以估计每种情况的延迟和并行性。将估计值与实际应用程序的经典分析所获得的测量结果进行比较。通过模型检查得出的延迟估计结果与测量结果非常接近，最好情况下的最小差异为 3.9%，最坏情况下的最小差异为 -26.8%。它还检测到测量的分析样本的随机性质未涵盖的有问题的执行路径。通过模型检查得到的并行度估计结果近似为最小差异为9.3%，最大差异为-28.8%。最后，将模型检查的工作量与实施和分析 RIS 的工作量进行比较。
This article introduces model checking as an alternative method to estimate the latency and parallelism of asynchronous Realtime Interactive Systems (RISs). Five typical concurrency and synchronization schemes often found in concurrent Virtual Reality (VR) and computer game systems are identified as use-cases. These use-cases guide the development a) of software primitives necessary for the use-case implementation based on asynchronous RIS architectures and b) of a graphical editor for the specification of various concurrency and synchronization schemes (including the use-cases) based on these primitives. Several model-checking tools are evaluated against typical requirements in the RIS area. As a result, the formal model checking language Rebeca and its model checker RMC are applied to the specification of the use-cases to estimate latency and parallelism for each case. The estimations are compared to measured results achieved by classical profiling from a real-world application. The estimated results of the latencies by model checking approximated the measured results adequately with a minimal difference of 3.9% in the best case and -26.8% in the worst case. It also detected a problematic execution path not covered by the stochastic nature of the measured profiling samples. The estimated results of the degree of parallelization by model checking are approximated with an minimal difference of 9.3% and a maximal difference of -28.8%. Finally, the effort of model checking is compared to the effort of implementing and profiling a RIS.