一句话：提出从非时间非概率分布式系统模型到概率时间模型的自动变换，并证明语义一致性，使定性与定量分析共享同一模型。
分布式系统需同时满足定性与定量性质，但前者常用 TLA+、Hoare/分离逻辑等非时间非概率框架分析，后者用 Uppaal、Prism 等时间/概率自动机框架分析。这导致同一系统需人工建立两个语义上未必一致的模型，且有限自动机难以表示无界数据结构、动态对象创建与无界消息等分布式对象系统特征。本文定义从一类非常一般的分布式系统（Agha actor 模型的推广）到概率时间模型的变换，将适合定性分析的非时间非概率模型映射为适合定量分析的模型，并证明二者语义一致。模型在重写逻辑中形式化，可用 Maude 做定性分析、PVeStA 做统计模型检验；变换已自动化并集成到 Actors2PMaude，通过自动转换多个分布式系统设计的定性模型来定量分析比较性能。
Today’s distributed systems must satisfy bothqualitativeandquantitativeproperties. These properties are analyzed using very different formal frameworks: expressive untimed and non-probabilistic frameworks, such as TLA+ and Hoare/separation logics, for qualitative properties; and timed/probabilistic-automaton-based ones, such as Uppaal and Prism, for quantitative ones. This requires developing two quite different models of the same system, without guarantees of semantic consistency between them. Furthermore, it is very hard or impossible torepresentintrinsic features of distributed object systems—such as unbounded data structures, dynamic object creation, and an unbounded number of messages—using finite automata.In this paper we bridge this semantic gap, overcome the problem of manually having to develop two different models of a system, and solve the representation problem by: (i) defining a transformation from a very general class of distributed systems (a generalization of Agha’s actor model) that maps an untimed non-probabilistic distributed system model suitable for qualitative analysis to a probabilistic timed model suitable for quantitative analysis; and (ii) proving the two models semantically consistent. We formalize our models in rewriting logic, and can therefore use the Maude tool to analyze qualitative properties, and statistical model checking with PVeStA to analyze quantitative properties. We have automated this transformation and integrated it, together with the PVeStA statistical model checker, into theActors2PMaudetool. We illustrate the expressiveness of our framework and our tool’s ease of use by automatically transforming untimed, qualitative models of numerous distributed system designs—including an industrial data store and a state-of-the-art transaction system—into quantitative models to analyze and compare the performance of different designs.
@article{paperbot1456,
title = {Bridging the semantic gap between qualitative and quantitative models of distributed systems},
author = {Si Liu and Jose Meseguer and Peter Csaba Ölveczky and Min Zhang and David Basin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563299}
}