安全工控程序分解与转换的形式化理论研究

The Industrial Control System (ICS), as the basic component of the automated production of the national economy and the people's livelihood, is a key part for national safe strategy. With the arrival of the Industry 4.0 and Internet+, the interaction between ICS and its network environment becomes more frequent, and the architecture of system becomes more complicated. It requires ICS with higher safety and intelligence, which brings new challenges to the development of safety-critical ICS software. In this project, we will adopt the formal method to design a model for ICS software with typical features. We propose a formal modelling language, and investigate its semantics. We also design a set of algebraic laws for the control program with multi physical device resource. And we can synthesize the control program from the unified model based on algebraic laws. We investigate a high intelligent and safe method for the ICS software development, which guarantees the safety and reliability of ICS software. The whole development cycle is supported by formal method technology. Our research not only enhance development efficiency, but also ensure software high quality, with great significance from the growth of ICS.

工业控制系统作为国计民生关键设施自动化生产的基础组件，是国家安全战略的重要组成部分。随着工业4.0、互联网+时代的到来，工控系统与外界网络环境的交互越来越密切，系统体系架构也越来越复杂，工控系统的安全性与智能化程度都亟需提高，这给安全关键工控系统软件的发展带来了新的挑战。本项目针对工控系统软件高安全性的要求，运用严格的形式化方法对具备典型特征的工控系统软件进行建模。研究形式化建模语言及其语义模型，设计适用于多物理设备资源的工控程序代数演算规则，完成软件模型的分解与转换，保证工控系统软件的安全性和可靠性，从而形成面向多物理设备资源的工控程序开发理论与方法。该开发方法全程由形式化方法作为技术支撑，不仅提高了开发效率而且保证了软件质量，对工控系统的发展具备重要的意义。

工业控制系统作为国计民生关键设施自动化生产的基础组件，是国家安全战略的重要组成部分。随着工业4.0、互联网+时代的到来，工控系统与外界网络环境的交互越来越密切，系统体系架构也越来越复杂，工控系统的安全性与智能化程度都亟需提高，这给安全关键工控系统软件的发展带来了新的挑战。本项目针对工控系统软件高安全性的要求，提出了一套完整的面向物理资源的工业控制系统软件开发方法；研究内容包括：工业建模协作语言，基于精化的模型框架，群体协作模型生成方法三个方面；解决了如何将物理设备资源与控制软件融于统一模型，控制软件分解与转换的可靠性的两大关键问题。研究成果在电力领域火力发电控制器研制过程中展开了示范应用。该开发方法全程由形式化方法作为技术支撑，不仅提高了开发效率而且保证了软件质量，对工控系统的发展具备重要的意义。本项目的研究成果形成学术论文13篇，其中SCIE-2区论文4篇、SCIE-4区论文1篇、CCF-C类论文8篇；申请发明专利4篇，获得软件著作权登记2项；协助培养博士研究生1名、硕士研究生3名。