机器人控制系统关键模块的形式化验证

• 作者: 关永 娄晨辉 李晓娟
• 来源期刊: 计算机测量与控制
• 关键词: 机器人控制系统 传感器数据采集模块 形式化验证 定理证明 微架构模型
• 年，卷（期）: 2016,（6）
• 所属期刊栏目: 试验与评价技术
• 页码范围: 315-318
• 页数: 4页
• 分类号: TP301
• 语种: 中文
• DOI: 10.16526/j.cnki.11-4762/tp.2016.06.086

摘要

随着机器人应用在越来越多的领域，人们对其安全性的要求越来越高，作为机器人的核心，控制系统设计的可靠性对整个系统的安全至关重要；针对一种模块化设计的机器人控制系统架构，利用 xMAS （eXecutable MicroArchitecture Specification，可执行微架构描述）模型在定理证明器ACL2中对其功能正确性进行验证，首先对Xmas 在ACL2中的形式化理论做了阐述，然后对该机器人控制系统中的加速度传感器数据采集模块建立xMAS模型，提取关键属性并进行验证；将xMAS模型和定理证明器ACL2相结合，可以很好地解决机器人控制系统的验证问题，为机器人控制系统的形式化验证提供一个有效的方法参考。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	关永	首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室轻型工业机器人与安全验证实验室	95	1336	17.0	33.0
2	李晓娟	首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室轻型工业机器人与安全验证实验室	39	261	9.0	14.0
3	娄晨辉	首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室轻型工业机器人与安全验证实验室	1	1	1.0	1.0