Unified property evaluations of constrained-devs models for simulation and model checking

Soroosh Gholami, Hessam S. Sarjoughian

Research output: Contribution to journalConference articlepeer-review


Properties represent the state of a system at any instance of time or for a period of time. We consider properties as a common concept for Experimental Frame (EF) that can be used for simulation and modeling checking. This affords to define experimental frames that can evaluate the dynamics of models of systems purposed for both validation and verification. We show this approach through simulation of Parallel DEVS models as well as model checking of Constrained-DEVS models. We develop experiments for simulating and model checking a prototypical Network-on-Chip (NoC) system. The models and experiments are developed and executed using the DEVS-Suite tool. New capabilities of this tool include support for defining experimental frames that stimulate and monitor executions of models. The proposed approach with the developed execution engine affords both simulation validation and model checking verification.

Original languageEnglish (US)
Pages (from-to)442-453
Number of pages12
JournalSimulation Series
Issue number2
StatePublished - 2021
Event2021 Annual Modeling and Simulation Conference, ANNSIM 2021 - Virtual, Online
Duration: Jul 19 2021Jul 22 2021


  • DEVS
  • Experimental Frame
  • Model Checking
  • Simulation
  • Validation
  • Verification

ASJC Scopus subject areas

  • Computer Networks and Communications


Dive into the research topics of 'Unified property evaluations of constrained-devs models for simulation and model checking'. Together they form a unique fingerprint.

Cite this