Formal Verification of Serial Port Module in Robot Control System

DOI

10.2991/emim-16.2016.156How to use a DOI?

Keywords

Robot control system; Serial module; Formal verification; Theorem proving

Abstract

As robots used in more and more fields, people are more striated with their safety. As the core of the mobile robot, the reliability of the control system is very important to the whole system. In this paper, a modular design of robot control system architecture is modeled by the xMAS (eXecutable MicroArchitectural Specication) and then verified using ACL2, proving the funtionality correctness. As the formalization of xMAS model in ACL2 is not complete, we first improve the formalization process in ACL2 and then establish xMAS model of the UART serial port module, abstract some key properties and verify them. Combination of the theorem prover ACL2 and xMAS model, which is a great way to solve the verification problem of robot control system, could also provide an effective reference method for the correctness verification of robot control system.

Copyright

© 2016, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Chenhui Lou
AU  - Xiaojuan Li
PY  - 2016/04
DA  - 2016/04
TI  - Formal Verification of Serial Port Module in Robot Control System
BT  - Proceedings of the 6th International Conference on Electronic, Mechanical, Information and Management Society
PB  - Atlantis Press
SP  - 753
EP  - 759
SN  - 2352-538X
UR  - https://doi.org/10.2991/emim-16.2016.156
DO  - 10.2991/emim-16.2016.156
ID  - Lou2016/04
ER  -