Projects

Sysfier
Developing SystemC Verifier

• Developing an integrated environment for modeling and verifying SystemC designs by formalizing SystemC semantics and providing model checking tools. Rebeca is used as the intermediate language and Rebeca verification tool set is used as the back-end model checkers.

Rebeca Verifier
Developing a tool suit for model checking Rebeca codes

• Developing translators to use back-end model checkers: NuSMV and Spin
• Developing LTL Model Checker
• Developing CTL Model Checker
• Investigating and applying reduction techniques in model checking Rebeca codes:
  • Compositional Verification
  • Symmetry reduction
  • Partial order
  • Slicing
• Using Artificial Intelligence in Model Checking
• Mapping Rebeca to Process Algebra and using mCRL2 for verification

Rebeca Modeling tool support

• Proposing a UML profile and a tool for mapping UML diagrams to Rebeca
• Developing a tool to map Rebeca models to Java codes in a distributed platform

Modeling and Verification of Security Protocols using Rebeca

Investigating the Analyzability of the Coordination Language Reo

• studying different semantics of Reo and classifying different kinds of priorities which can be considered in Reo and constraint automata

Modeling Web Services using Reo

• mapping BPEL and WS-CDL to Reo and analyze the model using constraint automata
• Conformance checking

Using Reo and constraint automata for hardware/software co-design