嵌入式控制软件的形式化规格说明构建的工程方法

在当前的工业界嵌入式控制软件开发领域，形式化方法的实际应用仍面临许多现实困难。从软件需求分析角度看，存在如下主要问题：1)缺乏面向领域的合适的形式化建模语言。2)缺乏系统化的形式化规格说明构建的工程方法。3) 形式化规格说明有效性(validity)检测手段不完善,效率低，缺乏实用的手段。 面对这一挑战，我们提出一种构造嵌入式控制软件形式规格说明的形式工程方法。受国家自然科学基金青年基金资助，课题执行期间取得了如下研究成果：1）提出了一种面向嵌入式控制软件需求建模的轻量级形式化建模语言；2）结合形式化工程方法，建立了一种演化式的形式化模型构建方法，提高了形式化建模过程的效率；3）提出了一种基于图形的需求审查方法，有效地提升了需求审查的错误探测能力；4）提出了一种基于场景的需求模型测试方法，支持在需求分析阶段即可进行仿真分析；5）研发了面向轨道交通车辆控制软件的需求建模工具，使得该方法在企业获得直接应用，显示了该方法具有明确的工程应用价值。

针对形式化方法在工业界嵌入式控制软件开发过程中难以有效应用的问题，本课题主要研究嵌入式控制软件的形式化规格说明构建工程方法，建立工程化形式化规格说明构建过程，并通过规格说明审查和测试保障规格说明的一致性和有效性。主要研究内容包括：为嵌入式控制软件形式化规格说明语言SPARDL提供与形式化语义一致的图形化描述；建立图形化描述引导的形式化规格说明工程化构建过程，引导开发者从原始需求出发通过不同阶段构建形式化规格说明；研究规格说明审查以保证规格说明的一致性；研究规格说明测试技术以保证规格说明的有效性。研究测试用例生成、测试过程动画模拟及测试结果分析等方法；开发相应的软件工具。课题将丰富当前的形式化建模理论与方法，为工业界嵌入式控制软件的开发者提供有效而实用的形式化规格说明构建工程方法。该课题对提高嵌入式控制软件的质量有重要意义，研究成果可有效推动形式化方法在工业界嵌入式控制软件开发中的实际应用。

从建筑设计到建成过程中，既符合力学规律，又遵循结构特征；同时也符合从艺术审美角度去审视其自身所应具有的美学法则；加之能在建造实施过程中保持其以上特征的过程。

建构包括设计、构建、建造等内容，是一个三位一体的集合，是一个全过程的综合反映。2100433B

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

(1)多功能模块处理：在一个复杂的具有多台变压器的变电站里，每台主变压器和每一段母线都可能独立运行，也可能并列运行。因此VQC的调节与控制应能适用各种运行方式下的调节。

(2)电压与无功的上下限值动态变化：对应于不同的高峰和低谷时段，电压与无功的上下限值应不同，以适应逆调压和无功功率调节的要求。

(3)调节方式的多样性：由于变电站中有时变压器或电容器组需要停运检修，因此考虑VQC调节时，调节方式应设置“只调电压”或“只调电容器”。对于控制策略中出现的矛盾，应能“智能”变化。例如有时电容器组已经全部投入或退出运行，这时已无电容器可调，应能“智能”地改为有载分接头的相应调节。软件VQC还应设置“只监视不控制”方式，以适应运行需要，它相当于只投入运行不投连接片的保护运行方式。

(4)实现远方控制VQC：就地VQC应能接受调度端的控制，实现投退某个电容器组或有载调节变压器的分接头。

(5)闭锁条件有如下几条：

1)保护闭锁。在对变压器有载调压分接头开关和电容器组监视控制过程中，如监测到系统及变压器、母线、电容器发生故障和异常的保护信号，应立即闭锁VQC的调节。

2)遥测闭锁。当遥测值超过VQC要求的范围时，闭锁VQC。

3)遥信闭锁。当变电站主接线运行方式改变时，闭锁VQC。

4)其他闭锁。VQC的TV断线，主变压器调压控制器、电容器组的控制回路断线或异常时，闭锁VQC。

(6)相关信号上送调度：软件VQC应适应无人值班变电站的需要，把一些必要的信号，如VQC调节闭锁、调节拒动、调节动作信号上送调度端以便于远方管理。

(7)并列运行、拒动、滑档等：在变压器并列运行时，VQC应使并列的变压器有载分接头开关同步操作。母线并列时对应的软件模块也应做并列的相应处理。主变压器有载分接头开关拒动、滑档时应立即停止调节并发出拒动和滑档的信号上送调度，多次拒动、滑档时应闭锁相应操作。

(8)登录操作：每一次调节都应有相应的记录，包括对象、动作类型、时间、调节结果等。