| 机器人控制系统关键模块的形式化验证 |
| |
| 作者姓名： | 娄晨辉 李晓娟 关永 |
| |
| 作者单位： | 首都师范大学 高可靠嵌入式系统技术北京市工程研究中心 电子系统可靠性重点实验室 轻型工业机器人与安全验证实验室,北京 100048,首都师范大学 高可靠嵌入式系统技术北京市工程研究中心 电子系统可靠性重点实验室 轻型工业机器人与安全验证实验室,北京 100048,首都师范大学 高可靠嵌入式系统技术北京市工程研究中心 电子系统可靠性重点实验室 轻型工业机器人与安全验证实验室,北京 100048 |
| |
| 基金项目： | 国家自然科学基金项目(61373034);北京市自然科学基金(4122017)。 |
| |
| 摘 要： | 随着机器人应用在越来越多的领域,人们对其安全性的要求越来越高,作为机器人的核心,控制系统设计的可靠性对整个系统的安全至关重要;针对一种模块化设计的机器人控制系统架构,利用xMAS(eXecutable MicroArchitecture Specification,可执行微架构描述)模型在定理证明器ACL2中对其功能正确性进行验证,首先对Xmas在ACL2中的形式化理论做了阐述,然后对该机器人控制系统中的加速度传感器数据采集模块建立xMAS模型,提取关键属性并进行验证;将xMAS模型和定理证明器ACL2相结合,可以很好地解决机器人控制系统的验证问题,为机器人控制系统的形式化验证提供一个有效的方法参考。
|
| 关 键 词： | 机器人控制系统 传感器数据采集模块 形式化验证 定理证明 微架构模型 |
| 收稿时间： | 2016-03-17 |
| 修稿时间： | 2016-04-12 |
|
| 点击此处可从《应用声学》浏览原始摘要信息 |
|
点击此处可从《应用声学》下载全文 |
|
