Techniques of Modeling and Analysis

1. TECHNIQUES OF MODELING AND ANALYSIS

Identification, simulation and formal verification are three modeling techniques and analysis of automatic systems. Some of the objectives of these techniques is to reduce and eliminate errors in the evolution of an automated system.

1.1. Identification

1.1.1. Definition

Identification is a technical study of discrete systems based on a basic concept: observability.

1.1.2. Usage

This technique can be applied to validate the integration of specifications (tests) or to obtain a model of behavior for an immediate result of the model.

1.1.3. Approaches

In the case of an automated system that includes a controller and an identification process can be done in two ways:

-by the observations of the controller in situ that interacts with the real process (this is used in diagnostic techniques), figure 1.a.;

-by the observations of the controller libre or „open loop” wich responds to the change of the inputs value that are excited for a specific identification (preferred solution for testing), figure 1.b.;

Figure1. Modes of identification: a. whith process; b. whithout process.

In the field of systems with discrete events, classical formalism is used for identifying finite state machine or with extensions such as Petri nets.

In the diagnosis-based model that is to identify the differences between the signals observed on a system running with signals from a pattern of behavior, identification is an experimental approach to obtain a model system.

Model behavior of the system may be a working model or a model that includes errors.

For obtain models of behavior are two other ways:

-building models based on knowledge of the functioning of the system (knowledge-based models);

-building a model based on collecting data generated during operation of the system (models based on data collection).

1.2. Simulation

1.2.1. Definition

Simulation can be defined as:

-A discipline of designing a model of an actual or theoretical physical system, executing the model on a digital computer, and analyzing the execution output. Simulation embodies the principle of ``learning by doing'' --- to learn about the system we must first build a model of some sort and then operate the model.

-Imitation of some real thing, state of affairs, or process. The act of simulating something generally entails representing certain key characteristics or behaviours of a selected physical or abstract system.

-A technique that allows testing of a finite number opportunities and relatively small for the evolution of an automated system. So the obtained results are valid only for certain scenarios of evolution.

1.2.2. Usage

Simulation is used in many contexts, including the modeling of natural systems or human systems in order to gain insight into their functioning. Other contexts include simulation of technology for performance optimization, safety engineering, testing, training and education. Simulation can be used to show the eventual real effects of alternative conditions and courses of action.

In many developed simulation is considered a good thing, a more or a less complex way and a model process, for example:

-[BARESI and others 1998] [BARESI and others 2000] where the process is modeled with blocks Simulink;

-[AMERONGEN 2003] where the process is modeled with bond graphic;

-[BARTON 1992] if the process is split into separate entities and each is modeled by a finite automaton;

-[MATTSSON and others 1998] [ELMQVIST and others 1999] where the process is modeled with Modelica language;

-[LIU, 2004] if it proposes a methodology for modeling process, SPOA (System Performance-Oriented Automation).

1.2.3. Approaches

In the main objectiv of simulation there are three sub-fields: model design, model execution and model analysis.

1.3. Formal verification

1.3.1. Definition

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

1.3.2. Usage

Formal verification can be used for example for systems such as cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

The verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.

1.3.3. Approaches

There are roughly two approaches to formal verification.

The first approach is model checking. This is an automated technique that, given a finite-tate model of a system and a property stated in some appropriate logical formalism (such as linear temporal logic LTL or computational tree logic CTL), systematically checks the validity of this property. Model checking is a general approach and is applied in areas like hardware verification and software engineering. Due to its success in several projects and the high degree of support from tools, there is an increasing interest in industry in model checking – various companies have started their own research groups and sometimes have developed their own in-house model checkers. For instance, Intel has started 3 validation laboratories for the verification of new chip designs. An interesting aspect of model checking is that it supports partial verification: a desing can be verified against a partial specification by considering only a subset of all requirements.