同步数据流语言pre算子在Coq中的翻译验证  

Translation Verification of Synchronous Data Stream Language Pre Operator in Coq

作　　者：李春燕 赵长名 杨斐 马权[2] 侯荣彬 LI Chunyan;ZHAO Changming;YANG Fei;MA Quan;HOU Rongbin(College of Computer,Chengdu University of Information Technology,Chengdu 610225 China;Science and Technology on Reactor System Design Technology Laboratory,Nuclear Power Institute of China,Chengdu 610041 China)

机构地区：[1]成都信息工程大学计算机学院,四川成都610225 [2]中国核动力研究设计院核反应堆系统设计技术重点实验室,四川成都610041

出　　处：《西华大学学报(自然科学版)》2025年第2期87-95,共9页Journal of Xihua University:Natural Science Edition

基　　金：四川省重点研发计划项目“面向电力领域的规划评审知识库智能构建关键技术研究”(2021YFG0307);四川省科技计划资助(2019ZDZX0001)。

摘　　要：文章对同步数据流语言的pre算子进行详细处理,除了将pre算子翻译至fby算子,还对pre算子在第一周期的值根据其输入参数类型的不同做了相应的初始化,解决了pre算子第一周期为空的问题。输入参数为整型和布尔型,其第一周期初始化为false,浮点型初始化为浮点零;数组和结构体类型,根据其元素类型分别进行不同的初始化。由于pre算子的翻译应用场景大多在核电安全级数字化控制系统(SDCS),因此为了确保其编译的正确性及安全性,整个翻译过程在辅助定理证明器Coq完成了形式化验证。同时该翻译及验证方法在SDCS中进行试用,达到了预期的翻译效果。The pre operator of the synchronous data stream language is processed in detail.In addition to translating the pre operator to the fby operator,the value of the pre operator in the first cycle is initialized according to the type of its input parameters in order to avoid that the first cycle of the pre operator is empty.The input parameters whose type are integers and booleans are initialized to false,and those of floating-point types are initialized to floating-point zero.Those of array and structure types are initialized differently according to their element types.The translation application scenarios of the pre operator are mostly nuclear power safety digital control systems(SDCS).In order to ensure the correctness and safety of its compilation,the entire translation process has undergone strict formal verification,and all of them are in the auxiliary theorem prover Coq completed in.The translation and verification method has been tested in SDCS,and can achieve the expected translation effect.

关 键 词：同步数据流语言 可信编译器 形式化验证 

分 类 号：TP314[自动化与计算机技术—计算机软件与理论]