Formal and Operational Study of C-DEVS.
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.
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. 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.
REFERENCES
Gabriel A. Wainer, Discrete – Event Modeling and Simulation: A practioner’s Approach, 2009.
Zeigler.B.P Theory of modeling and simulation. New York: Wiley Interscience. 1976
Aminu.M, Approach to a Simulation virtual Machine: Object oriented implementation of DEVS and PDEVS. Master’s thesis, African University of Science and Technology, Nigeria, December 2009.
SIMAUD, DEVS Standardization, Boston MA, April 5, 2011.
Jeannette M.Whing, A specifier’s Introduction to Formal Methods, September 1990.
Anthony Hall, “Realizing the Benefits of Formal Methods”, Independent consultant, UK.
StudentsandScholarship Team.
Be the first to comment