File Type: MS Word (DOC) & PDF

File Size: 1,178KB

Number of Pages:48

## ABSTRACT

C-DEVS is a formalism for modeling and analysis of discrete event systems. It refers to

the original formalism defined by Zeigler in 1976. While the simulation algorithms are

well defined, their implementation is a challenge due to both correctness and efficiency

issues. This work aims at studying the formalism and its operational semantics. We

review and validate the meta-model for SimStudio – a Java implementation of the DEVS

simulation protocol, and we debug its existing Java codes. We finally use formal methods

to perform model checking and theorem proving on the C-DEVS simulation system to

assess the properties of correctness.

** **

## TABLE OF CONTENTS

ACKNOWLEDGEMENTS ……………………………………………………………………………………………………………. 3

Abstract ……………………………………………………………………………………………………………………………….. 4

Chapter 1. Introduction ……………………………………………………………………………………………………… 8

1.1 DEVS formalism and its variants ………………………………………………………………………………….. 9

1.2 Formal analysis of DEVS simulation protocol. ………………………………………………………………. 10

1.3 Structure ……………………………………………………………………………………………………………….. 10

Chapter2. Discrete Even System Specification (DEVS) …………………………………………………………………. 11

2.1. DEVS (CDEVS and PDEVS with differences) ………………………………………………………………………. 11

2.2 CDEVS ………………………………………………………………………………………………………………………… 11

2.2.1 Classic DEVS (CDEVS) Atomic Model ………………………………………………………………………….. 11

2.2.2 Classic DEVS Coupled Model ………………………………………………………………………………. 13

2.3 Examples of CDEVS model and Simulation. ………………………………………………………………………. 14

2.4.The CDEVS Simulation Algorithm ……………………………………………………………………………………. 15

2.5. Example of CDEVS model and simulation (by hand)…………………………………………………………… 18

2.5.1 Simulation by hand ………………………………………………………………………………………………… 19

2.5.2 Simulation result Snapshot ………………………………………………………………………………………. 19

Chapter 3. Literature Review on PDEVS Implementations …………………………………………………………… 21

3.1 DEVS WITH SIMULTANEOUS EVENTS (PARALLEL DEVS) ………………………………………………………. 21

3.1.1 PDEVS Atomic Model ……………………………………………………………………………………………… 21

3.1.2. PDEVS Coupled Model ……………………………………………………………………………………………. 22

3.2 Survey of DEVS Implementations (with examples) …………………………………………………………….. 23

3.2.1 Simstudio implementation (meta – models) ……………………………………………………………….. 23

3.2.2 Comparison of approaches ………………………………………………………………………………………. 29

3.2.3 Problems with existing implementations ……………………………………………………………………. 30

Chapter 4. Formal Methods ……………………………………………………………………………………………………. 31

4.1 Introduction to formal methods ……………………………………………………………………………………… 31

4.2 Benefits of formal methods …………………………………………………………………………………………… 32

4.3 Survey of tools and methods ………………………………………………………………………………………….. 33

Chapter 5. Simstudio and Formal Methods ……………………………………………………………………………….. 34

5.1 Improvements on Simstudio ………………………………………………………………………………………….. 34

5.2. Towards integration of formal analysis with Simstudio………………………………………………………. 37

5.2.1 Formal Method: The B Method ………………………………………………………………………………… 37

5.2.2 UML to B ………………………………………………………………………………………………………………. 38

5.2.3 Formal specification of Simstudio ……………………………………………………………………………… 39

5.3 Use of formal tools with Simstudio: The Atelier B ………………………………………………………………. 43

5.4 Results and Discussions …………………………………………………………………………………………………. 44

Chapter6. Conclusions …………………………………………………………………………………………………………… 47

Challenges: ………………………………………………………………………………………………………………………….. 47

Future work: ………………………………………………………………………………………………………………………… 47

REFERENCES: ……………………………………………………………………………………………………………………….. 48

## CHAPTER ONE

Introduction

Many natural systems in physics, astrophysics, chemistry and biology, and human

systems in economics, psychology, social science and engineering have long relied on the

unsuitable methods for their study during the twentieth century. Traditional mathematical

methods such as differential equations have been used for centuries as the main tools for

analysis, comprehension, design, and prediction for complex systems in varied areas.

The emergence of computers simulation provided alternative methods of analysis for

both natural and artificial systems. Since the early days of computing, users translated

their analytical methods into computer-based simulation to solve with a level of

complexity unknown in earlier stages of scientific development.

Computational methods based on differential equations could not be easily applied in

studying human-made dynamic systems such as traffic controllers, robotic arms,

automated factories, production plants, and computer networks and so on. These systems

are usually referred to as discrete-event systems because their states do not change

continuously but, rather, because of the occurrence of events. This makes them

asynchronous, inherently concurrent, and highly nonlinear, rendering their modeling and

simulation different from that used in traditional approaches [1].

A number of techniques were introduced in order to improve the model definition for this

class of systems, Petri Nets, Finite state Machines, min-max algebra, Timed Automata,

and others [1].

Let us define the following key words.

Model: A model is a simplified representation of a system at some particular point in

time or space intended to promote understand of the real system.

System: A system exits and operates in time and space.

Simulation: A simulation is the manipulation of a model in such a way that it operates on

time or space to compress it, thus enabling one to perceive the interactions that would not

otherwise be apparent because of their separation on time or space.

Modeling and Simulation (M&S) is the use of models, including emulators, prototypes,

simulators, and either statically or over time, to develop data as a basis for making

managerial or technical decisions. The primary motivation for modeling and simulation is

risk reduction, that is, to ensure that the simulation can support its user/developer

objectives acceptably. This is the primary benefit in cost-benefit concerns about

Verification and Validation (V & V), which is the core issue in the question of how much

V & V is needed.

Modeling and simulation play increasingly important roles in modern life. It contributes

to our understanding of how things function and are essential to the effective and efficient

design, evaluation, and operation of new products and systems. Modeling and simulation

results provide vital information for decisions and actions in many areas of business and

government. Verification and validation are processes that help to ensure that models and

simulations are correct and reliable. Although significant advances in V&V have

occurred in the past 15 years, significant challenges remain that impede the full potential

of modeling and simulation made possible by advances in computers and software.

1.1 DEVS formalism and its variants

DEVS (Discrete Event System Specification) defined by Zeigler in the 1970’s is one of

the existing theories of Modeling and Simulation allowing the modular description of

discrete event models. It finds a way to specify systems whose states change either upon

the reception of an input event or due to the expiration of a time delay. In order to attack

the complexity of the system under study, the model is organized hierarchically (i.e., it is

organized in a way such that every element is higher than its precedent), and higher-level

components of the system are decomposed into simpler elements.

The separation between model and simulator and the hierarchical and modular nature of

the formalism have enabled carrying out of formal proofs on the different entities under

study. One of them is the proof of composability of the subcomponents (including

legitimacy and equivalence between multicomponent models). The second is the ability

to conduct proofs of correctness of the simulation algorithms, which results in simulators

rigorously verified. The proofs are based on formal transformations (morphisms) between

each of the representations, trying to prove the equivalence between the entities under

study at different levels of abstraction. For instance, we can prove that the mathematical

entity simulator is able to execute correctly the behavior described by the mathematical

entity model, which represents the system under the experimental framework (which can

also be represented formally).

Numerous extensions of the classic DEVS formalism have been developed in the last

decades. Among them formalisms which allow having changing model structures while

the simulation time evolves:

G-DEVS, Parallel DEVS, Dynamic Structuring DEVS, Cell-DEVS [2], dynDEVS,

Fuzzy-DEVS, GK-DEVS, ml-DEVS, Symbolic DEVS, Real-Time DEVS, rho-DEVS

[Wikipedia].

We will present DEVS with further details in the following chapter.

1.2 Formal analysis of DEVS simulation protocol.

The use of formal analysis for DEVS simulation protocol is motivated by the expectation

that, as in other engineering disciplines, performing appropriate mathematical analysis

can contribute to the reliability and robustness of the algorithm. The most likely reason

for this is that the formal analysis leads into relatively simple and independent

components, which allow for straightforward unit testing of model checking and theorem

proving on the C-DEVS simulation protocol to assess the properties of correctness and

efficiency. We recall that the simulation protocol of DEVS models considers two issues:

time synchronization and message propagation. Time synchronization of DEVS is to

control all models to have the identical current time. However, for an efficient execution,

the algorithm makes the current time jump to the most urgent time when an event is

scheduled to execute its internal state transition as well as its output generation. Message

propagation is to transmit a triggering message which can be either an input or output

event along the associated couplings which are defined in a coupled DEVS model.

1.3 Structure

We organize our work as follows: Chapter_2 describes the Discrete Event System and

Specification for CDEVS and PDEVS, Chapter_3 is the literature review on PDEVS

implementations and the use of the Unified Modeling Language (UML) for the

implementation of Simstudio (meta- model). In Chapter_4 we introduce the formal

methods, the benefits of the formal methods and survey of tools and methods. Chapter_5

describes the use of formal methods and survey of tools with Simstudio then Chapter_6

concludes our work and presents challenges and the future work to be done.