FORMAL ANALYSIS OF DDML
Need help with a related project topic or New topic? Send Us Your Topic
DOWNLOAD THE COMPLETE PROJECT MATERIAL
FORMAL ANALYSIS OF DDML
ABSTRACT
In order to test and evaluate the attributes of DEVS Driven Modelling Language (DDML) models, we present a framework for formal analysis of DDML models.
This framework semantically maps the DDML hierarchical levels of Input Output System (IOS), Input Output Relation Observation (IORO), and Coupled Network (CN) to the corresponding formal methods of Labelled Transition System (LTS),
Linear Temporal Logic (LTL), Computation Tree Logic (CTL), and Communicating Sequential Processes (CSP). We employ formal tools (such as JTORX, LTSA, PAT, and NUSMV) to automatically analyse these formal specifications to evaluate attributes of DDML models at each level of abstraction.
CHAPITRE ONE
Introduction
This paper proposes a framework for explicitly assessing and evaluating DDML models. DDML is a modelling language intended for use with the DEVS modelling and simulation (M & S) framework.
Modelling and simulation is a large subject of study that applies to computer science by using computer-assisted and monitored simulation for real-world problems in science and engineering.
Computer simulation applications span a wide range of fields and are useful for studying real-world systems in order to obtain knowledge and make strategic decisions.
Before delving into the meat of this book, it is necessary to provide an overview of the M & S sector and explain its significance, applications, and concepts.
1.1 Simulation and modelling
Modelling and simulation is a paradigm that gives a means of depicting problems and reasoning about them in order to propose a solution or technique or absorb relevant facts to solve them.
Modelling and simulation have five basic principles that assist define the process and the components of the process. The following are definitions of such concepts:
An Object is a physical entity that exists in the actual world and has a definite structure and behaviour.
A system is a well-defined thing in the actual world that exists under certain conditions that specify specific characteristics of its structure and behaviour.
A model is a simplified depiction of an object’s properties, structure, and behaviour. This representation may be logical, mathematical, or physical in nature.
The experimental frame describes the experimental conditions in which the model will be employed. It incorporates the experiment’s objectives as well as the features of the model to be tracked.
Simulation: the execution of a model in order to obtain information about changes in the system’s behaviour, structure, and properties during executions. It aids in observing and inferring the system’s dynamic behaviour by displaying the execution of these dynamic behaviours across time.
Modelling and simulation are the processes of creating a model of a real-world system and then working on the model to study and absorb new information. In computer science, modelling and simulation are used to explore the attributes, structure, and behaviour of systems, as well as to obtain and infer new knowledge about them.
Modelling and simulation are widely used in many fields of science, including business, to analyse events and activities using models that are similar to real-world settings.
For essential systems such as aviation, health care, medication manufacture, electrical/electronic systems, oil production, supply chain management and logistics, military intelligence and defence systems, virtual testing of models is cheaper, possible, and even safer to research.
Formal Analysis of DDML Soremekun Olamide Ezekiel Page 5 However, in computer science, modelling and simulation can be utilised at many phases of development, from requirements engineering to design, implementation, project management, and installation. The figure below depicts the application of modelling and simulation in the subject of computer science.
Figure 1 depicts the application of modelling and simulation in the field of computer science. Benefits Modelling and simulation can provide numerous benefits to both the user and the environment at large.
Modelling and simulation assist the user in better understanding the system, optimising system performance, and ensuring the reliability and safety of such systems. Different limitations and circumstances that cannot be checked in the real world can be checked by the user using modelling and simulation.
For example, simulation of their models can be used to undertake life-critical scenarios in the health-care system, drug use, or even microscopic level of detail evaluation of materials.
Furthermore, modelling and simulation have been used to assist validate systems, with models of current systems being ran and mistakes or defects being checked to avert their devastating occurrence in real life.
Models of Europe’s road and rail transport systems, as well as the United States’ air traffic control system, have been evaluated and verified using modelling and simulation [1, 2].Soremekun Olamide Ezekiel Formal Analysis of DDML Page 6
Furthermore, modelling and simulation are critical for the effective design and evaluation of systems, as they aid in the development of a dependable and well-designed product or system.
This is accomplished by evaluating the proposed system’s operation through its model over time and enhancing its performance by modifying the system’s constraints and conditions in order to compute the optimal set of constraint variables for the best performance.
The impacts of changing conditions on the system can thus be determined without altering the real system or having to create the system to check for such changes. Figure 2 is a diagram that summarises the multiple benefits of modelling and simulation in modern culture.
Finally, modelling and simulation can be used to solve real-world problems as well as unanticipated or future arising flaws in systems. The temporal effect of long processes can be compressed using simulation to see the various future outcomes of processes and problems that may occur during future operation.
Identifying such flaws can assist in making critical corporate and government decisions about the system in order to avoid flaws or potential future disasters.
Aside from that, a real-life problem, such as the spread of a specific disease, can be modelled and the spread can be stopped by recording the rate or direction of spread through simulation and implementing necessary decisive methods to prevent this.Figure 2 depicts the multiple benefits of modelling and simulation.
Formal Analysis Of DDML
Ezekiel Olamide Soremekun The Importance of Page 7 The significance of modelling and simulation is based on its advantages. It is significant since it aids in the cost-effectiveness of system testing.
Modelling and simulations are less expensive than building the system and running test cases on it; this would entail building many duplicate systems because systems can be destroyed after each test case. However, with a good system model, test cases may be conducted without having to spend a lot of money constructing the same system over and over again.
Aside from that, Modelling and Simulation (M & S) gives a level of detail that is scaleable to the size of the system. A model can represent a system as large as the universe or as small as a microscopic environment with a high level of information that is critical to the experimental frame.
This level of detail is significant since it may not be feasible in the real system with current technology, but it may be obtained through models, and significant information about the behaviour of such real-world systems can even be deduced from such models.
This scale flexibility is a fundamental advantage of modelling and simulation. It gives this type of system experimentation a competitive advantage.
Challenges Every paradigm has its own set of constraints and obstacles. Modelling and computer simulation can be constrained by a computer’s memory, processing speed, or other resources.
Another significant constraint may be the amount of data available to accurately depict the system. The capacity to precisely and efficiently describe the real-life system with the best features, structure, and behaviour that appropriately depict the system is a major challenge for M & S. A lack of this precise representation may result in model mistakes and, as a result, simulation problems.
Another M & S challenge is using an inappropriate simulation algorithm or programme, which results in simulation errors or inaccurate behaviour. erroneous simulation programmes may offer users with erroneous information about the system’s behaviour, attributes, and structure.
As a result, the user will infer incorrect data about the system, resulting in a faulty simulation result. As a result, the process’s legitimacy would be called into question. Finally, it may be difficult to appropriately analyse simulation results and draw crucial or accurate information from them.
Verifying and confirming the simulation results may be futile, and interpreting some results in real life may be challenging.
The modelling and simulation method’s power is in the right interpretation of its outcomes; difficulties interpreting these results could render the entire process ineffective.
1.2Introduction to DDML and DEVS
The Discrete Event System Specification (DEVS) is a modelling formalism that has grown in importance and popularity in modelling and simulation, owing to the fact that various formalisms have been shown to have equivalent DEVS representations.
Despite the fact that DEVS is especially designed to simulate discrete events, it has been demonstrated that discrete time events and differential (continuous) event systems can be simply converted to DEVS.
DEVS is especially significant because of its modular architecture, which promotes component/concern separation (model, simulator, and experimental frame).
Furthermore, DEVs are semi-formal, allowing for freedom and flexibility of application; modellers are free to freely represent the structure, behaviour, and traces of their system. DDML (DEVS modelling language) is a graphical and hierarchical formalism used to create dynamic system models for simulation.
DEVS inspired the development of DDML, which was designed to capture the structure and behaviour of systems by focusing on three layers of abstraction: the Input Output System (IOS), the Coupled Network (CN), and the Input Output Relation Observation (IORO).
1.3 Formal Methods
A formal specification is the statement of a group of qualities that a system should satisfy in some formal language and at some level of abstraction. It is critical to consider the concept of specifications relative to the problem domain (rather than the solution domain).
To ensure that a solution addresses an issue appropriately, the problem must first be stated accurately. A formal specification language offers the mathematical foundation for a formal procedure.
A specification is formal if it is expressed in a language composed of three components: rules for determining sentence grammatical well-formedness (the syntax); rules for interpreting sentences in a precise, meaningful way within the domain under consideration (the semantics); and rules for inferring useful information from the specification (the proof theory).
Formal specification techniques differ from semi-formal ones in that the latter do not formalise the assertion part: an assertion part in which the intended properties on the declared variables are formalised.
A formal specification language includes a notation (its syntactic domain), a universe of objects (its semantic domain), and a precise rule that specifies which objects satisfy each specification. A specification is a phrase written in terms of syntactic domain elements.
1.4 Structure Of Thesis Report
DDML Formal Analysis
Ezekiel Olamide Soremekun Page 9
The remainder of this paper is organised as follows. Chapters 1–4 serve as an introduction to the work completed. In chapter 2, we present a brief overview of DDML, including syntax and semantics.
Chapter 3 looks at the field of formal techniques, including a study of its concepts and paradigms, benefits, and a summary of formal tools utilised in this work. The following collection of chapters expands on the introductory subjects and serves as a foundation for the work done.
After exploring the relevance, techniques, and issues involved in combining formal methods and simulation in the first three chapters, we link these concepts in chapter 4 by discussing the importance, approaches, and challenges involved in mixing formal methods and simulation.
Furthermore, this chapter emphasises the significance of employing a variety of formal procedures in the course of our work.
In Chapter 5, we provide a formal framework for DDML, rationalise our choice of formal methods at each level of abstraction, and provide a semantic mapping/translation of each formal method to each level of DDML abstraction.
The majority of the work is demonstrated in Chapter 6 by presenting the formal analysis of DDML models at all three levels of abstraction via a traffic light case study.
Finally, chapter 7 presents an overview of the work, the obstacles involved, the necessity to integrate the tools, and a glimpse into the future work that will be done on this subject.
In this chapter, we discuss our plans to provide a tool for automatic code creation for formal analysis, as well as the architecture for this platform.
Need help with a related project topic or New topic? Send Us Your Topic