AI 中文总结
本文提出Constraint-DEVS方法，扩展DEVS-Suite框架以支持离散事件系统的仿真与模型检查，开发并验证了片上网络模型，为该框架的混合引擎提供了设计制品。
AI 中文摘要
验证与确认（V&V）是评估动态模型需求及规格、确保其实现预期目标的关键方法。并行离散事件系统规范（PDEVS）是一种基于系统理论的建模方法，用于创建模块化、分层的基于组件的仿真模型。本文提出了Constraint-DEVS方法，用于创建有界并行DEVS模型，该模型除了可用于仿真外，还支持模型检查。我们扩展了DEVS-Suite框架以创建Constraint-DEVS规格，随后可通过所提出的结合并行DEVS抽象仿真器协议的状态探索协议对其进行模型检查。这些功能，加上对非确定性、复杂数据传输及性能相关属性检查的支持，使Constraint-DEVS及其配套的DEVS-Suite成为开发、验证和确认离散事件系统的独特框架。为展示该工作，我们开发并验证了片上网络（Network-on-Chip）模型，同时详细说明了DEVS-Suite框架的混合模型检查与仿真引擎的行为设计制品。
英文摘要
Verification and validation (V&V) are crucial methods for evaluating the requirements and specifications of dynamical models that fulfill their intended purposes. Parallel Discrete EVent System Specification (PDEVS) is a system-theoretic modeling approach for creating modular, hierarchical component-based simulation models. In this paper, we introduce Constraint-DEVS, a method for creating bounded Parallel DEVS models that lend themselves, in addition to simulation, to model checking. We extend the DEVS-Suite framework to create Constraint-DEVS specifications which can then be model checked using a proposed state exploration protocol with the Parallel DEVS abstract simulator protocol. These capabilities, along with the support for non-determinism, complex data transfer, and performance-related property checking, make Constraint-DEVS and its accompanying DEVS-Suite a unique framework for the development, verification, and validation of discrete-event systems. In order to demonstrate this work, we developed and verified models of Network-on-Chip. Also, we detail behavioral design artifacts for the DEVS-Suite framework's hybrid model-checking and simulation engine.
Comments33 pages, 19 figures, 6 tables, 2 listings
