Modeling and verification of network-on-chip using constrained-DEVS

Soroosh Gholami, Hessam Sarjoughian

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


Verification of models is necessary for some classes of systems to guarantee safety properties in addition to satisfying functional requirements. Exhaustive model checking is a full proof method for verifying lack of undesirable behavior for dynamical systems. In this work, we present a model checking verification method for Network-on-Chip (NoC) models. For this purpose, a constrained version of the atomic DEVS modeling formalism is formulated and applied to verification of an NoC router. This is achieved by adding constraints on the state size and the number of transitions in the atomic model. A model-checker is introduced into the DEVS-Suite simulator for verifying constrained DEVS models using the DEVS simulator protocol. The model-checker is used to verify a model of NoC router component at different scale. The state space size, number of state transitions, and execution time metrics, without and with fault, demonstrate the verification of constrained DEVS models.

Original languageEnglish (US)
Pages (from-to)97-108
Number of pages12
JournalSimulation Series
Issue number4
StatePublished - 2017


  • Constrained-DEVS
  • DEVS-Suite simulator
  • Model checking
  • Network-on-Chip
  • Verification

ASJC Scopus subject areas

  • Computer Networks and Communications


Dive into the research topics of 'Modeling and verification of network-on-chip using constrained-DEVS'. Together they form a unique fingerprint.

Cite this