Project File Details


Original Author (Copyright Owner): 

3,000.00

Instant Download

Download your project material immediately after online payment.

100% Money Back Guarantee

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.

 

GET THE FULL WORK

DISCLAIMER: All project works, files and documents posted on this website, projects.ng are the property/copyright of their respective owners. They are for research reference/guidance purposes only and the works are crowd-sourced. Please don’t submit someone’s work as your own to avoid plagiarism and its consequences. Most of the project works are provided by the schools' libraries to help in guiding students on their research. Use it as a guidance purpose only and not copy the work word for word (verbatim). If you see your work posted here, and you want it to be removed/credited, please call us on +2348157165603 or send us a mail together with the web address link to the work, to hello@projects.ng. We will reply to and honor every request. Please notice it may take up to 24 or 48 hours to process your request.