CAJ | 학술논문

Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效提高编译器的安全性。因为Lustre程序是并发执行的，需要对其进行因果分析和串行化。利用Coq工具，形式化定义拓扑排序的性质和相应层次的Lustre的语义；对Lustre程序进行因果分析和排序；证明排序后的程序满足拓扑排序的性质；证明任意两个满足拓扑排序性质的程序语义执行等价。从而实现了一种针对Lustre程序的可信排序过程。
Lustre시일충엄범응용우핵전、항공등고가신영역적동보수거류어언。용형식화험증적방법래실현Lustre도C적번역병증명기과정능유효제고편역기적안전성。인위Lustre정서시병발집행적，수요대기진행인과분석화천행화。이용Coq공구，형식화정의탁복배서적성질화상응층차적Lustre적어의；대Lustre정서진행인과분석화배서；증명배서후적정서만족탁복배서적성질；증명임의량개만족탁복배서성질적정서어의집행등개。종이실현료일충침대Lustre정서적가신배서과정。
Lustre is a synchronous data-flow language which is widely applied in nuclear power and aviation,all are in the areas with high credibility.The safety of the compiler will be significantly improved by applying the formal verification approach to implementing the translation from Lustre to C and proving its procedure.Because the Lustre program executes concurrently,the causality analysis and sequentialisation on it is necessary.In the paper,we implement a credible sorting procedure for Lustre program,which is completed by in the first formally defining the property of topological sorting and the Lustre semantics in associate layers with Coq tool,doing the causality analysis and sorting on Lustre program,then proving that a sorted Lustre program fulfils the property of topological sorting,and finally proving that any two Lustre programs both of which satisfying the property of topological sorting are semantically equivalent in execution.