| COQ定理证明器辅助PLC 程序验证和分析 |
| |
| 引用本文： | 陈钢,宋晓宇,顾明.COQ定理证明器辅助PLC 程序验证和分析[J].北京大学学报(自然科学版),2010,46(1):30-34. |
| |
| 作者姓名： | 陈钢 宋晓宇 顾明 |
| |
| 作者单位： | 1. Lingcore Laboratory, Portland, OR97224; 2.Department of ECE, Portland State University, Portland, OR97207; 3. 清华大学软件学院, 北京100084; |
| |
| 基金项目： | 国家自然科学基金资助项目(90718039) |
| |
| 摘 要： | 使用定理证明器COQ 验证和分析PLC 抢答器程序的一些性质, 证明了原程序的所有可能状态中只有半数是可达状态, 揭示了系统在可达状态之间的转移关系。基于这些性质, 引入了逻辑自动机的概念作为对PLC程序行为完整抽象的描述。此外, 在证明过程中, 发现该程序中存在着一个很难通过现场测试发现的问题。
|
| 关 键 词： | 可编程序控制器 PLC 嵌入式系统 COQ 定理证明 |
| 收稿时间： | 2009-01-05 |
PLC Program Verification and Analysis Using the COQ Theorem Prover |
| |
| CHEN Gang,SONG Xiaoyu,GU Ming.PLC Program Verification and Analysis Using the COQ Theorem Prover[J].Acta Scientiarum Naturalium Universitatis Pekinensis,2010,46(1):30-34. |
| |
| Authors: | CHEN Gang SONG Xiaoyu GU Ming |
| |
| Institution: | 1. Lingcore Laboratory, Portland, OR97224; 2. Department of ECE, Portland State University, Portland, OR97207; 3.School of Software, Tsinghua University, Beijing 100084; |
| |
| Abstract: | |
| |
| Keywords: | programmable logic controller PLC embedded system COQ theorem proving |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《北京大学学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《北京大学学报(自然科学版)》下载免费的PDF全文 |
|
