The DEVS formalism: a framework for logical analysis and performance evaluation for discrete event systems

This paper proposes a framework which supports performance evaluation and logical analysis of discrete event systems using a unified formalism, i.e., the DEVS (discrete event system specification) formalism. For performance evaluation, DEVSim++, a realization of the DEVS formalism and the associated simulation algorithms in C++, is used. For logical analysis, the dual language approach is adopted. We use the DEVS formalism as an operational formalism to describe system´s behavior. Temporal logic (TL) is employed as an assertional formalism to specify system´s properties. To reduce states space in logical analysis, we exploit a projection mechanism. The method is a mapping of a set of states in models into a state which obtained from TL assertions. An example of logical analysis for alternating bit protocol is given.<>