Tool

jRESP is a Java runtime environment providing a framework for developing autonomic and adaptive systems according to the SCEL paradigm. Specifically, jRESP provides an API that permits using in Java programs the SCEL’s linguistic constructs for controlling the computation and interaction of autonomic components, and for defining the architecture of systems and ensembles.

jRESP also provides specific components that can be used to simulate SCEL programs. In particular, to support analysis of adaptive systems specified in SCEL, jRESP provides a set of classes that permits simulating jRESP programs. These classes allow the execution of virtual components over a simulation environment that is able to control component interactions and to collect relevant simulation data.

Robot-swarm Simulation

Robot-swarm Simulation

By relying on jRESP simulation environment, a prototype framework for statistical model-checking has been also developed. Following this approach, a randomized algorithm is used to verify whether the implementation of a system satisfies a specific property with a certain degree of confidence. Indeed, the statistical model-checker is parametrized with respect to a given tolerance ε and error probability p. The used algorithm guarantees that the difference between the value computed by the algorithm and the exact one is greater than ε with a probability that is less than p. The model-checker included in jRESP can be used to verify reachability properties. These permits evaluating the probability to reach, within a given deadline, a configuration where a given predicate on collected data is satisfied.


Link: