Today's distributed systems must satisfy both
\emph{qualitative} and \emph{quantitative} properties. 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 to \emph{represent}
intrinsic 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 the
\emph{Actors2PMaude} tool.
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.