Projects

CRYSTAL

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

Consistency of Distributed Controllers

In distributed control systems, multiple primary controllers in redundancy plans can lead to inconsistency. In this project we model and formally verify the NRP FD algorithm. We identify an issue and propose a solution to enhance the robustness and reliability of such systems. Learn more

RoboRebeca: Dependble ROS application

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

HybridRebeca

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

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

AdaptiveFlow

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

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

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

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

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

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

Core Rebeca

In this project we provide a formal semantics and model checking toolset for Rebeca modeling language. Rebeca is an actor-based language for modeling concurrent and reactive systems with asynchronous message passing. Learn more