Projects

SEADA Logo

SEADA

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

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

wRebeca

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

Tangramob Logo

Tangramob

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

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

PTRebeca

PTRebeca

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

TARO

TARO

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

TR2RTMaude

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

Sysfier

Sysfier

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