Formal Modeling And Verification For Component-Based Model Integrated CNC Systems With IEC 61499 Standard

With the rapid development and tight connection of information technology and mechanical industry, equipment manufacture as the leader and core of industry development has been the critical area to realize the modernization of industry in China. To speed up the core techniques of equipment manufacture and develop the advanced manufacturing technology, computer numerical control systems as the pivot of the high-grade NC machine tools is developing at the flexibility, intelligence and networks. How to guarantee the CNC systems development efficient, responsible and complete, while not to waste a lot of time and money needs the innovation for the development approaches of CNC systems. The traditional development methods of CNC systems have been thrown out, while a formal modeling and verification approach for embedded CNC systems is built up with IEC 61499 and formal methods through the component-based model integrated development method to provide the safe, fast and effective development solution for the CNC systems.The component-based model integrated method and formal methods have been studied in detail. Aiming to the domain specific characteristics and demands, the formal framework for embedded CNC sytems is proposed. The whole framework can be divided into two parts, i.e. the formal modeling framework and the formal verification framework. The formal modeling framework is established by a CNC formal modeling language from the completed CNC domain specific models to attain the formal models of CNC systems. The formal verification framework is to specify the characteristics of systems in a formal way through a formal specification language, to produce the formal specification of the system properties and to combine the formal models into model checking to check whether the formal models are satisfied with the functionality and performance demands of CNC systems.Aiming to the formal modeling framework of CNC systems, the literal or graphic components of the domain specific models are defined by the formal models with explicit syntax and semantics through the hierarchical modeling thoughts of IEC 61499 and formal specification methods to realize the clear and unambiguous specification for components and the interaction rules between components and even to satisfy the determinacy and consistency of the components dynamic behaviors during the execution process of systems. Besides, the syntax assignment from the domain specific models to CNCFML, the anchor of syntax and semantics in CNCFML and the semantics assignment from CNCFML to the formal models are defined in detail to complete the model transformation from the domain specific models to the formal models to facilitate the simulation and formal verification in the model layer of the CNC systems.Aiming to the formal verification framework, a CNC formal specification language integrated with the input-output function based on the functionality verification and the computation tree logic based on the performance verification is advanced to describe the functionality requirements of application and the non-functionality requirements of system. The combination of the formal models and formal specifications can be used to simulate the functionality of the application on the Ptolemy II and verify the non-functionality properties of the system on UPPAAL.Lastly, the two development cases are given by the developed formal framework, CNCFML and the formal verification methods, i.e. drilling test equipment and CNC cutter control systems. The domain specific models are built up on the CORFU which is the model integrated environment based on IEC 61499. Applying with the semantics assignment, the formal models as the semantic models in the each layer of the domain specific models are generated. The formal models of the application are constructed on the Ptolemy II and the formal models of the system are constituted on the UPPAAL. Then the formal models are checked on the responding tools to verify the requirements of systems during the execution process. In the end, the formal modeling and verification approach has been demonstrated to be suitable for the development of the multi functions and high performance CNC systems.This dissertation attempts to introduce the formal methods and component-based model integrated methods into the CNC systems by proposing the formal framework, CNCFML and the formal verification methods. Further research will probably provide the fast, efficient and responsible development pattern and solutions for the requirements specification, model design, code generation and implementation of the embedded control systems. And it’s helpful for the reusability and reconfiguration of components. This effort is important to enhance the level of the advanced manufacturing technology in equipment manufacture area.