The Modelling and Verification of PLC Program Based on Interactive Theorem Proving Tool COQ
作者单位：National Laboratory for Information Science and Technology Key Laboratory for Information System Security Ministry of EducationDepartment of Computer Science and Technology School of Software Tsinghua University Beijing Special Engineering Design and Research Institute National Laboratory for Information Science and Technology Key Laboratory for Information System Security Ministry of Education Department of Computer Science and Technology School of Software Tsinghua University
会议名称：《2011 International Conference on Computer Science and Information Technology(ICCSIT 2011)》
会议日期：2011年
学科分类：08[工学] 0802[工学-机械工程] 0835[工学-软件工程] 080201[工学-机械制造及其自动化]
基 金：sponsored by NSFC Program (No.90718039 & No.91018015) 973 Program(No.2010CB328003) of China
关 键 词：PLC Program Embedded System Verification Denotational Semantics Theorem Proving COQ
摘 要：COQ is an interactive theorem proving tool. The paper abstractly describes the feature of COQ, the architecture and working modes of PLC program with the example of typical PLC. It also introduces the first-order logic syntax and semantics of Intuitionistic Logic. It briefly introduces the main Gallina language syntax elements, the corresponding use methods and main theorem proving tactic on COQ. The work has modeled kernel data type and basic statements and and the denotational semantics of PLC program with Gallina. It has given the correctness proof of PLC program based on theorem proving, i.e. based on semantics function the relationship of configuration between the before codes execution and the after is proved. The main purpose is to prove whether a PLC program satisfies certain nature within a scan period.