面向服务的数控系统形式化建模与验证技术研究

In order to describe the complex interaction semantic between heterogeneous CNC function service and verify the correctness of CNC system, this project proposes a service-oriented formal modeling and verification method, which employ the interface automata theory to accomplish abstract modeling for CNC function service and study the interaction semantic relating to service composition accordance with the hierarchical structure by Model of Computation (MoC). For the formal modeling of the non-functional system constraints such as real-time, security and etc., a hybrid computation tree logic Integrated with qualitative and quantitative expression is introduced and the by use of model verification technology the verification of the correctness of the overall system can be realized. Finally, to further optimize the verified system, the optimization design of CNC function service composition is discussed based on the theory of multiobjective optimization. In summary, this project is aimed at the establishment of an engineering method for CNC system design under service-oriented architecture.

针对SOA架构下，异构数控功能服务间复杂交互语义描述及系统正确性验证等问题，提出一种面向服务的数控系统形式化建模与验证方法。所提方法基于接口自动机理论对数控功能服务进行抽象建模，并且利用计算模型依据层次化的结构对服务组合交互行为语义进行分析和描述。同时针对实时性、安全性等非功能系统约束，提出利用兼具定性和定量表达的计算树逻辑建立系统约束的形式规约，并结合模型检验技术从整体上实现对数控系统正确性的验证。最后为实现已验证数控系统服务质量的最优化，提出从多目标角度解决数控功能服务组合的优化设计问题。面向服务的数控系统形式化建模与验证技术的研究旨在利用形式化方法建立一套SOA架构下设计实施数控系统的工程化方法，对构建基于SOA的高性能数控系统具有重要的指导意义。

本研究针对异构数控功能服务间复杂交互语义描述及系统正确性验证等问题，提出一种面向服务的数控系统形式化建模与验证方法。首先在数控功能的服务化封装，组合语义建模等面向服务系统设计实施过程中的核心问题方面，提出面向服务的开放式数控系统设计框架，其通过结合领域建模、形式化语义描述和多目标优化等关键技术，遵照服务建模、服务组合与验证、组合模型优化的系统设计流程，将各阶段的设计工作集成到统一的框架中；然后通过深入研究IEC 61499参考模型与面向服务架构间的映射关系，提出利用领域建模技术来解决面向服务的数控系统设计过程中的应用系统建模问题，为保证元模型的精确性，在研究中采用形式化描述方法来指导元模型的设计，并基于多维关注分离、端口和接口嵌套等设计策略，分别对数控领域特征、IEC 61499参考模型和SOA组成要素等不同侧面的子领域信息进行元模型设计，通过定义各方面信息间的映射与关联规则，最终构建具备多元信息融合特征的、面向服务的复合化数控领域元模型；在语义建模阶段，选择同步反应（SR）、离散事件（DE）、时间多任务（TM）等三类典型的实时并发计算模型来实现数控服务组合语义的建模，通过计算模型间的组合、连接或嵌套实现层次化异构的语义描述；另外从多目标优化角度出发，以加工误差、加工速度和资源利用率等不同方面的服务质量为参考，建立面向数控服务组合的多目标优化模型，并根据物联网及智能制造的特点提出了新一代数控系统移动服务化的基本架构。最后以某特定型号的微钻为例，对所构建的控制系统的实际加工效果进行了测试，验证了本研究所设计方法的可行性和有效性。