随着信息技术与机械工业的高速发展与紧密结合,装备制造业作为我国工业发展的排头兵与核心力量,已经成为我国实现工业现代化的关键领域。加快发展装备制造业的核心技术,大力开发先进制造技术,尤其针对高档数控机床的控制中枢——计算机数控系统(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上构造系统的形式化模型,通过在相应工具上的仿真验证,验证了系统模型在运行过程中满足诸多系统需求,从而论证了本文提出的形式化建模与验证方法论适用于多功能、高性能嵌入式数控系统的开发。本文提出的嵌入式数控系统的形式化框架、形式化建模语言以及形式化仿真验证方法是将形式化方法和组件化模型集成开发方法应用在数控领域的一个尝试。对该方法的深入研究可能为嵌入式控制系统的需求描述、模型设计以及代码产生和实施等开发过程提供快速、高效和可靠的开发模式和研究途径,并有利于系统中组件的可复用性和可重配置性,对提升我国装备制造业的先进制造技术具有重大意义。