The advancement in computer technology has led to the development of new highly sophisticated Computer Numerical Control machines known as CNC machines. CNC machine is a system in which a control microcomputer is an integral part of the machine that controls the movements of the machine components. Thus this advancement in modern CNC machines makes this technology highly sophisticated, costly, complex, and need a great deal of training. The problem raised is that training on these highly sophisticated machines is very expensive, and without proper training, new operators may injure themselves or cause damages to these expensive machines. I'o overcome this problem, it was obvious that there is a clear need for new technologies to assist in training on CNC machines. In this thesis, we investigated the available technologies that can provide an effective training method for workers that are al the same level of training on an actual machine. It was found that Virtual Reality, VR, is an effective technology to develop training modules where a virtual environment of the CNC machine replaces the actual one in the real world, 'braining in the virtual environment gives trainees the freedom to explore the CNC machine and make errors without the worry of injuries or damages. Next, we designed a virtual training CNC machine system, with the milling machine being the chosen example. However, during the design phase and from the review of the previous applications of VR as training models for CNC machines, we found out that very little was validated. 'I'his means that no technique was used to insure the VR CNC model will react as an actual machine at runtime. Thus, this will affect the transfer of learning of the workers. Therefore. we strongly believe that there is a clear need to test the virtual model for validation before applying it for training purposes. We also believe that formal methods make it possible to describe the virtual model to be developed in an accurate and unambiguous way. Furthermore, it was found that formal methods were used in other application domain than manufacturing. Hence, we investigated and used formal methods (in particular the logic-base ITL and its executable subset) in specifying and verifying the elementary CNC system. T’his has been achieved by viewing the CNC system as a single mathematical function transforming points into machine tool displacement. Thus, we came up with a prototype system of the CNC milling machine that is self-validated. Finally, we evaluated our virtual CNC machine with a number of case studies of machining different engineering components with various shapes. We chose primitive shapes since our approach is compositional, Therefore, complex shapes can be validated al runtime by decomposing them into a number of simpler shapes.