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. 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

wRebeca Logo

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). Learn more

Tangramob Logo

Understanding the impacts of a mobility initiative prior to deployment is a complex task for both urban planners and transport companies. To support this task, Tangramob offers an Agent-Based (AB) simulation framework for assessing the evolution of urban traffic after the introduction of new mobility services. This allows urban planners and transport companies to evaluate the efficacy of their initiatives with respect to the current urban system. In this project, we simplified the Tangramob model into a Timed Rebeca (TRebeca) model and we designed ToolTRain, i.e. a tool-chain. Learn more


PTRebeca language is developed for supporting the modeling and verification of real-time systems with probabilistic behaviors. The syntax of PTRebeca is a combination of pRebeca and TRebeca. We propose the appropriate semantics for PTRebeca to be able to model and verify probabilistic properties. In a probabilistic assignment, a value is assigned to the variable with the specified probability. Notably, by using probabilistic assignment, the value of the timing constructs (delay, after, and deadline) can also become probabilistic. Learn more


TARO (Timed Rebeca)
In TARO (Timed Asynchronous Reactive Objects in Distributed Systems) project, we proposed to develop a methodology, techniques and tools, for building fully asynchronous systems, whose behaviour depends crucially on timing constraints, with associated formal analysis and verification support. Our methodology is based on proposing an actor-based modeling language, extended with timing constraints and supported by formal verification tools, called Timed Rebeca. Learn more


Timed Rebeca to Real-Time Maude
Although Rebeca is supported by a rich verification toolset, Timed Rebeca has not had an executable formal semantics, and has therefore had limited support for formal analysis. In this project we provide a formal semantics of Timed Rebeca in Real-Time Maude to resolve this limitation. We have automated the translation from Timed Rebeca to Real-Time Maude, allowing Timed Rebeca models to be automatically analyzed using Real-Time Maude's reachability analysis tool and timed CTL model checker. Learn more


Verification Facilities for Hardware-Software Codesign Approach
The goal of Sysfier is to develop an integrated environment for modeling and verifying SystemC designs by formalizing SystemC semantics and providing model checking tools. The tool Afra is developed as SystemC modeling and analysis environment. Afra gets SystemC models and LTL or CTL properties from the designer, and verifies the models. Where applicable, reduction techniques are used to tackle the state explosion problem. Learn more