Modeling Language for the Integration of Parallel Discrete Event Simulation Modeling and Parallel Model Checking
DOI:
CSTR:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    The correctness and reliability of parallel discrete event simulation models play an important role in the development of PDES. Most of the existing PDES developing environments do not support model verification at present. The completeness and high effectiveness of parallel model checking helps it successful in making its way into industrial tools. While PDES and PMC are implemented in different modeling languages, in the current practice, to check whether or not a PDES model contains any errors, a prototype that is solely written for model checking purposes has to be built. This process is an onerous, time-consuming and error-prone task. The current research presented a modeling language, namely Extended Event Graph (EEG) to combine PDES and PMC, and it extended the classical event graph in aspect of synchronization. This modeling language makes it possible for users to achieve PDES and PMC with only one model via transformation mechanisms, thus saving both the time and effort of developers. The experimental results confirm the validity of this language and it can support both PDES and PMC.

    Reference
    Related
    Cited by
Get Citation
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:June 16,2011
  • Revised:
  • Adopted:
  • Online: September 12,2012
  • Published:
Article QR Code