“School of Computer Science”

Back to Papers Home
Back to Papers of School of Computer Science

Paper   IPM / Computer Science / 10869
School of Computer Science
  Title:   Modere: the model-checking engine of Rebeca
  Author(s): 
1.  M. M. Jaghoori
2.  A. Movaghar
3.  M. Sirjani
  Status:   In Proceedings
  Proceeding: SAC
  Year:  2006
  Pages:   1810 - 181
  Publisher(s):   ACM
  Supported by:  IPM
  Abstract:
Rebeca is an actor-based language with formal semantics that can be used in modeling concurrent and distributed software and protocols. Automatic verification of these systems in the design stage helps develop error free systems. In this paper, we describe the model checking tool developed for verification of Rebeca models. This tool uses partial order reduction technique for reducing the size of the state space generated for a given model. Using this tool for model checking Rebeca yields much better results than the previous attempts for model checking Rebeca.

Download TeX format
back to top
scroll left or right