Replicated Computations Results (RCR) Report for "Design and Verification of Trusted Collective Adaptive Systems"

The article "Design and Verification of Trusted Collective Adaptive Systems" by Aldini proposes a process-algebraic framework for modeling and verifying trusted collective adaptive systems. To favor reuse, the system and trust models can be specified separately, only to be integrated at the semantic level. Through a combination of behavioral equivalence checking and model checking against branching-time temporal logic with trust predicates, the framework allows comparative analyses of different trust models as well as analyses of the effects of attacks to the trust models. The applicability of the formal framework is illustrated by means of two representative use cases: the security analysis of a trust-incentive service management system and a comparison of two different reputation systems. This replicated computations results report focuses on the reproducibility of the experiments performed in the aforementioned article, i.e. on the automatic verification of properties against models of these use cases encoded in the well-known NuSMV model checker. It was straightforward to reproduce all results from the article in reasonable time using a standard laptop machine.