西华大学学报（自然科学版）2025，Vol.44Issue(2)：87-95,9.DOI:10.12198/j.issn.1673-159X.5024
同步数据流语言pre算子在Coq中的翻译验证
Translation Verification of Synchronous Data Stream Language Pre Operator in Coq
摘要
Abstract
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 float-ing-point types are initialized to floating-point zero.Those of array and structure types are initialized differ-ently 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.关键词
同步数据流语言/可信编译器/形式化验证Key words
synchronous dataflow language/trusted compiler/formal verification分类
计算机与自动化引用本文复制引用
李春燕,赵长名,杨斐,马权,侯荣彬..同步数据流语言pre算子在Coq中的翻译验证[J].西华大学学报（自然科学版）,2025,44(2):87-95,9.基金项目
四川省重点研发计划项目"面向电力领域的规划评审知识库智能构建关键技术研究"(2021YFG0307) （2021YFG0307）
四川省科技计划资助(2019ZDZX0001). （2019ZDZX0001）
