【作者】 涂钰青；

【导师】 李迪；

【作者基本信息】 华南理工大学 ， 机械电子工程， 2011， 博士

【摘要】 随着信息技术与机械工业的高速发展与紧密结合,装备制造业作为我国工业发展的排头兵与核心力量,已经成为我国实现工业现代化的关键领域。加快发展装备制造业的核心技术,大力开发先进制造技术,尤其针对高档数控机床的控制中枢——计算机数控系统(Computer Numerical Control Systems, CNC Systems)的设计与开发,正朝着柔性化、智能化和网络化的方向发展。如何保证数控系统的开发在不牺牲大量时间和资源的前提下,能够达到高效、可靠和完备的特点,这需要一种面向数控系统开发方法论的革新。本文摒弃了数控系统的传统开发方法,借鉴组件化模型集成开发方法,采用IEC 61499标准的组件库和形式化方法,建立一套面向嵌入式数控系统建模和验证的形式化开发方法,为数控系统的开发提供安全、快速和有效的解决方案。在对组件化模型集成方法和形式化方法进行深入研究的基础上,针对数控系统的领域特性和系统需求,提出了面向嵌入式数控系统的形式化框架。整个框架包括两个部分:形式化建模框架和形式化验证框架。形式化建模框架从已构建形成的组件化模型集成数控系统的领域模型出发,通过构造面向数控系统的形式化建模语言(CNC Formal Modeling Language,CNCFML),实现领域模型到形式化模型的模型转换。形式化验证框架通过形式化描述语言,对系统特性进行形式化规约,产生系统相关性质的形式化描述,与形式化模型一起进行模型检验,以检验系统设计模型是否满足功能和性能需求。针对数控系统的形式化建模框架,结合IEC 61499层次化建模思想和形式化描述方法,将领域模型中文字式或图形化的组件定义为具有精确语法和语义的形式化模型,实现对组件和组件间交互方式清晰、无歧义的描述,以满足系统在执行过程中组件动态行为的确定性和一致性。另外,通过设计领域模型到CNCFML的语法指定、CNCFML的语法语义锚和CNCFML到形式化模型的语义指定,完成领域模型到形式化模型的转换,有利于系统模型层的形式化仿真和验证。针对数控系统的形式化验证框架,提出一种基于功能验证的输入输出函数和基于性能验证的计算树逻辑(Computation Tree Logic,CTL)集成的数控系统描述语言(CNC Formal Specification Language,CNCFSL),用来描述应用模型的功能需求和系统模型的非功能属性需求,并联系形式化建模框架中应用和系统的形式化模型,完成基于Ptolemy II工具中应用的功能仿真和基于UPPAAL工具中系统的非功能属性验证。最后,采用所设计研究的数控系统的形式化框架、建模语言和验证方法,给出了两个开发实例:钻孔检测一体机和数控平面切割机控制系统。在基于IEC 61499的模型集成环境CORFU上构造系统的领域模型,通过CNCFML的语义指定生成相应的形式化模型作为领域模型中各层的语义模型,并在Ptolemy II上构造应用的形式化模型,在UPPAAL上构造系统的形式化模型,通过在相应工具上的仿真验证,验证了系统模型在运行过程中满足诸多系统需求,从而论证了本文提出的形式化建模与验证方法论适用于多功能、高性能嵌入式数控系统的开发。本文提出的嵌入式数控系统的形式化框架、形式化建模语言以及形式化仿真验证方法是将形式化方法和组件化模型集成开发方法应用在数控领域的一个尝试。对该方法的深入研究可能为嵌入式控制系统的需求描述、模型设计以及代码产生和实施等开发过程提供快速、高效和可靠的开发模式和研究途径,并有利于系统中组件的可复用性和可重配置性,对提升我国装备制造业的先进制造技术具有重大意义。更多还原

【Abstract】 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.更多还原