SEADA: Self-Adaptive Actors

In SEADA we will use Ptolemy to represent the architecture, and extensions of Rebeca for modeling and verification. Ptolemy is a modeling and simulation tool for cyber-physical systems where the components are actors and the communication and coordination of actors are captured in a director which represents the Model of Computation. Rebeca is an actor-based modeling language with formal verification support. In SEADA, we will propose a framework for self-adaptive systems with a component-based architecture built in Ptolemy II. Our models@runtime will be coded in an extension of Probabilistic Timed Rebeca (with dynamic features), and supporting tools for customized run-time formal verification of these models will be developed. more

wRebeca: Efficient Modeling of Mobile Ad hoc Networks

wRebeca is an actor-based modeling language, an extension of Rebeca, proposed for modeling and verification of Mobile Ad Hoc Networks (MANETs). It is supported by the tool, which efficiently generates the state spaces of models. Several techniques have been exploited to reduce the state spaces like counting abstraction (which is sound in case the underlying topology is static), and removal of un-observable transitions (which preserves the ACTL-X properties of the original model). more

PTRebeca: Probabilistic Timed Actors

TARO: Timed Asynchronous Reactive Objects in Distributed Systems (Timed Rebeca)

Sysfier: Verification Facilities for Hardware-Software Codesign Approach