A Framework for Verifying Discrete Event Models Within a DEVS-Based System Development Methodology

摘要

This paper proposes a framework for verifying discrete event models using a dual specification approach. The approach employs two specifications for a discrete event model: an operational specification for the behavior of a model and an assertional specification for its temporal properties. The DEVS(Discrete Event System Specification) formalism is employed for the operational specification and Temporal logic(TL) is used for the assertional specification. A model's verification is based on a language acceptance checking mechanism for which TL constitutes a language grammar and DEVS models act as string generators. To demonstrate the proposed framework, verification of a communication protocol model is exemplified. The role of the framework within a larger DEVS-based methodology for system development is also discussed.