CRYSTAL mainly focuses on assessing the security aspects of Cyber-Physical Systems. In this project, we use Timed Rebeca and model checker Afra to specify and verify the behavior of CPS components against CPS-related attacks. We analyze architecture of CPS design to recognize where the potential attacks can successfully lead the system to security violation. Learn more



In SEADA (Self-Adaptive Actors) we will use Ptolemy to represent the architecture, and extensions of Rebeca for modeling and verification. Our models@runtime will be coded in an extension of Probabilistic Timed Rebeca, and supporting tools for customized run-time formal verification of these models will be developed. Learn more

RoboRebeca Logo


RoboRebeca is a framework which provides facilities for developing safe/correct source codes for robotic applications. In RoboRebeca, models are developed using Rebeca family language and automatically transformed into ROS compatible source codes. This framework is integrated into Afra 3.0. Learn more

wRebeca Logo


Hybrid Rebeca, is an extension of actor-based language Rebeca, to support modeling of cyber-physical systems. In this extension, physical actors are introduced as new computational entities to encapsulate the physical behaviors. Learn more

Tangramob Logo


Tangramob offers an Agent-Based simulation framework (using Timed Rebeca) for assessing the evolution of urban traffic after the introduction of new mobility services. This allows planners and transport companies to evaluate the efficacy of their initiatives with respect to the current urban system. Learn more

Tangramob Logo


AdaptiveFlow is an actor-based eulerian framework for track-based flow management. Learn more

wRebeca Logo


wRebeca is an actor-based modeling language, an extension of Rebeca, proposed for efficient modeling and verification of Mobile Ad Hoc Networks (MANETs). It is supported by the tool, which efficiently generates the state spaces of models and benefits from several reduction techniques. Learn more



PTRebeca language is developed for supporting the modeling and verification of real-time systems with probabilistic behaviors. We propose the appropriate syntax and semantics for PTRebeca to be able to model and verify probabilistic properties. Learn more



In TARO (Timed Asynchronous Reactive Objects in Distributed Systems) project, we proposed an actor-based modeling language, extended with timing constraints and supported by formal verification tools, called Timed Rebeca, for systems whose behavior depends crucially on timing constraints. Learn more


TRebeca to RTMaude

In this project we provide a formal semantics and automatic transformation tool from Timed Rebeca to Real-Time Maude as its executable formal semantics. This way, Timed Rebeca models can be analyzed using RTMaude's reachability analysis tool and timed CTL model checker. Learn more



The goal of Sysfier is to develop an integrated environment for modeling and verifying SystemC designs (HW/SW co-design) by formalizing SystemC semantics and providing model checking tools. The tool Afra 1.0 is developed as SystemC modeling and analysis environment. Learn more