Formalization and Visualization of an Automatic Production Line

Verification and Validation (V&Y) of control software is nowadays assuming great significance in manufacturing systems, for it has been finally understood that a thorough study on this subject could mean a considerable improvement in the efficiency of production processes. For this reason V&V has become a necessity due to the pressures of market demand. Manufacturing companies tend to solve these market pressures by the use of testing. But it is not quite correct, due to the fact that testing is a heuristic methodology and it has not a scientific foundation. This thesis proposes another different methodology –a method consisting in the abstraction of the controlled object in a formal representation, –better known as "formalization". By means of formalization much more system information can be obtained and be used in the improvement of the efficiency of production processes. In this thesis the benefits of formalization are proven by the application of the methodology in a real case. It means that the formalization of a case study will be developed obtaining significant results that will prove their own benefits. After the formalization the system can be subjected to model-checking –where a lot of information can be extracted from. One of the results of this thesis is the obtaining of the state space and the timing diagram of the system. Furthermore in this thesis it is highlighted and exposed one of the possible applications of formal methods –the system simulation in a visual representation