Formal Analysis of DDML
ABSTRACT
We propose a framework for formal analysis of DEVS Driven Modeling Language (DDML) models in order to assess and evaluate the properties of DDML models. This framework semantically maps the hierarchical levels of DDML: Input Output system (IOS), Input Output Relation Observation (IORO) and Coupled Network (CN) levels to corresponding formal methods: Labeled Transition System (LTS), Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), and Communicating Sequential Processes (CSP) respectively. These formal methods capture the semantics of DDML at each level of abstraction and we use formal tools (such as JTORX, LTSA, PAT and NUSMV) to automatically analyze these formal specifications to evaluate properties of DDML models at each level.
TABLE OF CONTENTS
Contents
Abstract ………………………………………………………………………………………………………………………………….. 2
Table of Content …………………………………………………………………………………………………………………………. 3
Chapter 1: Introduction ……………………………………………………………………………………………………………. 4
Chapter 2: The DEVS-Driven Modeling Language …………………………………………………………………………… 10
Chapter 3: Formal Methods ………………………………………………………………………………………………………… 16
3.1 Introduction to formal methods ……………………………………………………………………………………… 16
3.2 Benefits of formal methods ……………………………………………………………………………………………. 16
3.3. Survey of formal methods ……………………………………………………………………………………………… 17
3.4 Tools for formal analysis ………………………………………………………………………………………………… 20
Chapter 4: Combining Formal Methods and Simulation …………………………………………………………………. 21
4.1. Importance of combining formal methods with simulation ……………………………………………….. 21
4.2. Survey of approaches to combining formal methods with simulation …………………………………. 21
4.3. Challenges and the need to use multiple formal methods …………………………………………………. 22
Chapter 5: Formal Framework of DDML ……………………………………………………………………………………. 23
Chapter 6: Formal Analysis with DDML: A Case Study…………………………………………………………………….. 34
Tools …………………………………………………………………………………………………………………………………….. 63
LTSA tests ………………………………………………………………………………………………………………………….. 64
6.3 DDML CN test using Process Analysis Toolkit (PAT)……………………………………………………………….. 66
Chapter 7: Conclusions ………………………………………………………………………………………………………………. 73
CHAPTER ONE
Chapter 1: Introduction
The framework proposed in this work is intended to formally assess and evaluate DDML models. DDML is a modeling language designed to be used for the DEVS formalism of modeling and simulation (M & S). Modeling and simulation is a broad field of science applicable to computer science through computer automated and monitored simulation for real life problems in science and engineering. The applications of computer simulations cover a broad spectrum of fields and are relevant to study real life systems in order to gather information and make strategic decisions. In order to delve into the bulk of this work, it is important to give an overview of the M & S field and reveal its importance, uses and concepts.
1.1 Modeling and simulation
Modeling and simulation is a paradigm that provides a way of representing problems and reasoning about the problems in order to proffer a solution or method or absorb relevant data to solve such problems. Concepts There are five major concepts of Modeling and simulation that help define the process and the components of the process. Below is the definition of such concepts:
An Object: this is a certain entity that exists in the real world which has a specific structure and behavior.
A system: is a well defined object in the real world under specific conditions, which define specific aspects of the object’s structure and behavior.
A model: is an abstract representation of an object, its properties, structure and behavior. This representation could be logical, mathematical or physical.
Experimental Frame: the experimental frame defines the experimental conditions under which the model would be used. It encapsulates the objectives of the experiment and the aspects of the model to be tracked.
Simulation: is the execution of a model, in order to get information about the changes in the behavior, structure and properties of the system during the executions. It helps to observe and infer on the dynamic behavior of the system by showcasing the implementation of these dynamic behaviors over time.
Modeling and simulation refers to the process of producing a model of a real life system and the act of operating on the model in order to study and absorb new information. Modeling and simulation in computer science is used to study the properties, structure ad behavior of systems and to gather and infer new information concerning such systems. Modeling and simulation has become widely used in many aspects of science and even in business in order to study events and activities through models likened to the real world scenarios. This is because virtual experimentation of models is cheaper, possible and even safer to study for critical systems such as: aviation, health care, drug production, electrical/electronic systems, oil production, supply chain management and logistics, military intelligence and defense systems. However, in computer science modeling and simulation can be used
Formal Analysis of DDML
Soremekun Olamide Ezekiel Page 5
at many stages of development from the requirements engineering phase to the design, implementation, project management and the installation phase. Below is a diagram showing the use of Modeling and simulation within the computer science field.
Fig 1: the use of Modeling and Simulation in the Computer Science field Benefits Modeling and simulation can be of many benefits to the user and the world at large. Modeling and simulation helps the user to understand the system better, optimize the performance of the system and check for reliability and safety of such systems. With modeling and simulation, different constraints and conditions that can not be checked in the real world can be checked by the user. For example life critical scenarios in the health care system or drug use or even microscopic level of detail evaluation of material can be performed by simulation of their models. Furthermore, modeling and simulation has been a tool to help validate systems, models of existing systems are executed and errors or bugs are checked in order to avoid their disastrous occurrence in real life. For example, models of the road and rail transport system in Europe as well as the air traffic control system in the United States have been tested and validated through modeling and simulation [1, 2].
Formal Analysis of DDML
Soremekun Olamide Ezekiel Page 6
Furthermore, modeling and simulation is essential for the effective design and evaluation of systems, it helps to build a reliable and well designed product or system. This is achieved by studying the operation of the proposed system through its model over time and improving its performance by manipulating constraints and conditions that affect the system in order to compute the best set of constraint variable for the best performance. This way the effects of changes in conditions on the system can be determined without actually affecting the real system or having to build the system to check for such changes. The diagram shown below in figure 2 help summarize the numerous advantages of Modeling and simulation in our society. Finally, modeling and simulation provides a way to solve real life problems or even solve unforeseen or future resulting faults in systems. Through simulation, the time effect of long processes can be compressed in order to see the possible future outcome of processes and faults that can be generated in the course of future operation. Identifying such faults can help make important business and government decision concerning the system in order to avert faults or possible future disaster. Besides this, a real life problem like the spread of a particular disease can be modeled and the spread can be cut off by noting the rate or direction of spread through the simulation and applying necessary decisive strategies to avert this.
Fig 2: the numerous advantages of Modeling and Simulation
Formal Analysis of DDML
Soremekun Olamide Ezekiel Page 7
Importance The importance of modeling and simulation is pinnacled on its strengths. It is important because it helps in saving money in systems testing. Modeling and simulations is cheaper than building the system and performing test cases on the built system, this would involve building many duplicate systems has systems can be destroyed after each test case. However, with a good model of the system, test cases can be performed without the need to spend huge expenses building the same system over and over again. Besides this, Modeling and Simulation (M & S) provides a level of detail that is flexible to system size. A model can represent a system as big as the universe or as small as a microscopic environment with an efficient level of detail that is important to the experimental frame. This level of detail is important because it might not be achievable in the real system with the current technology but can be achieved through models and notable information about the behavior of such real life systems can even be inferred from such model. This flexibility in size is a major strength of modeling and simulation. It provides a cutting edge advantage for this form of system experimentation. Challenges Every paradigm has its limitations and challenges. Modeling and computer simulation can be limited by the capacity of computers in terms of memory, processing speeds or other resources. Another major limitation could be the amount of data available to accurately represent the system. A major challenge of M & S is the ability to accurately and efficiently represent the real life system with the best properties, structure and behavior that correctly depict the system. A shortage of this accurate representation may result in a model error and consequently simulation errors. Another M & S challenge is the use of an incorrect simulation algorithm or program; this would result in simulation errors or inaccurate behavior. Simulation programs that are incorrect could provide its users with wrong information on the behavior, properties and structure of the system. Subsequently, this would make the user infer wrong data about the system and creates a faulty simulation result. This would result in a process with a questionable credibility. Finally, it could be difficult to correctly interpret simulation results and to also infer important or accurate information form the simulation results. Verifying and validating the simulation results could prove abortive, and the understanding of some results in the real life might be difficult to attain. The strength of the modeling and simulation process lies in the correct interpretation of its result, challenges interpreting these results could make the entire process useless.
1.2 Introduction to DDML and DEVS
The Discrete Event System Specification (DEVS) is a modeling formalism that has become important and highly preferable in modeling and simulation; this is because other formalisms have been proven to have an equivalent DEVS representation. Even though DEVS is specifically designed to model discrete
Formal Analysis of DDML
Soremekun Olamide Ezekiel Page 8
events, it has been shown that discrete time events and differential (continuous) event systems can be easily converted to DEVS. DEVS is also important because of its modular architecture which promotes the separation of components/concerns (model, simulator and experimental frame). Furthermore, DEVs is semi formal which allows for freedom and flexibility of use, modelers are free to express the structure, behavior and traces of their system freely. DDML (DEVS modeling language) is a graphical and hierarchical formalism that is developed to construct models of dynamic systems for simulation. DDML is motivated by DEVS and it is developed to capture the structure and behavior of systems by focusing on the three levels of abstraction, the Input Output System (IOS) level, the Coupled Network (CN) level and the Input Output Relation Observation (IORO) level.
1.3 Formal methods
A formal specification is the expression, in some formal language and at some level of abstraction, of a collection of properties some system should satisfy. It is important to view the idea of specifications pertaining to the problem domain (as opposed to the solution domain). To make sure some solution solves a problem correctly, one must first state that problem correctly. A formal specification language provides a formal method’s mathematical basis. A specification is formal if it is expressed in a language made of three components: rules for determining the grammatical well-formedness of sentences (the syntax); rules for interpreting sentences in a precise, meaningful way within the domain considered (the semantics); and rules for inferring useful information from the specification (the proof theory). Formal specification techniques essentially differ from semi-formal ones (such as dataflow diagrams, entity-relationship diagrams or state transition diagrams) in that the latter do not formalize the assertion part: an assertion part, where the intended properties on the declared variables are formalized. A formal specification language provides a notation (its syntactic domain), a universe of objects (its semantic domain), and a precise rule defining which objects satisfy each specification. A specification is a sentence written in terms of the elements of the syntactic domain
1.4 Structure of thesis report
Formal Analysis of DDML
Soremekun Olamide Ezekiel Page 9
The rest of this report is structured as follows. Chapters 1, 2 and 4 provide an introductory section to the work done. In chapter 2 we provide a brief introduction to DDML, its syntax and semantics. Chapter 3 provides a look into the field of formal methods, a survey of its concepts and paradigms, its benefits and a summary of formal tools used in the course of this work. The next set of chapters builds on the introductory topics and provides a basis for the work done. Considering the introductory topics touched in the first three chapters, in chapter 4 we link these concepts by discussing the importance, approaches and challenges involved in combining formal methods and simulation. Furthermore, this chapter reveals the importance of using multiple formal methods in the course of our work. In chapter 5, we propose a formal framework for DDML and rationalize our choice of formal methods at each level of abstraction and provide a semantic mapping/translation of each level of DDML abstraction to each formal method. The bulk of the work is shown in chapter 6 by revealing the formal analysis of DDML models at all three levels of abstraction through a traffic light case study. Finally, chapter 7 provides a summary of the work, the challenges involved, the need to integrate the tools and a peep into the future work that would be continued on this work. In this chapter we reveal our intention to provide a tool for automatic code generation for formal analysis and propose architecture for this platform.
IF YOU CAN'T FIND YOUR TOPIC, CLICK HERE TO HIRE A WRITER»
