TwoTowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems

We present TwoTowers, a tool for analyzing functional and performance properties of concurrent systems expressed as terms in the stochastically timed reward process algebra EMPAr. TwoTowers builds on two existing tools, CWB-NC and MarCA, that have been retargeted to carry out functional and performance analysis (respectively) of EMPAr system specifications. As an example, we describe the application of TwoTowers to the Lehmann-Rabin randomized distributed algorithm for the dining philosopher problem