| PLC程序形式化的设计与验证 |
| |
| 引用本文： | 齐鹏飞,罗继亮,陈雪琨.PLC程序形式化的设计与验证[J].华侨大学学报(自然科学版),2013(3):241-246. |
| |
| 作者姓名： | 齐鹏飞 罗继亮 陈雪琨 |
| |
| 作者单位： | 华侨大学信息科学与工程学院 |
| |
| 基金项目： | 国家青年自然科学基金资助项目(60904018);福建省高等学校新世纪优秀人才支持计划项目(11FJRC01);福建省自然科学基金资助项目(2010J01339,2011J01352);福建省高校杰出青年科研人才培育计划项目(JA10004);中央高校基本科研业务费专项基金资助项目(JB-SJ1006) |
| |
| 摘 要： | 从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法.最后,比较将两种形式化方法应用到PLC程序的特点,探讨现有成果中存在的问题及研究发展方向.
|
| 关 键 词： | 可编程逻辑控制器 形式化设计 Petri网 自动机 定理证明 模型验证 |
| 本文献已被 CNKI 等数据库收录！ |
|
