Proceedings of the 6th International Conference on Electronic, Mechanical, Information and Management Society

Formal Verification of Serial Port Module in Robot Control System

Authors
Chenhui Lou, Xiaojuan Li
Corresponding Author
Chenhui Lou
Available Online April 2016.
DOI
https://doi.org/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.
Open Access
This is an open access article distributed under the CC BY-NC license.

Download article (PDF)

Proceedings
6th International Conference on Electronic, Mechanical, Information and Management Society
Part of series
Advances in Computer Science Research
Publication Date
April 2016
ISBN
978-94-6252-176-6
ISSN
2352-538X
DOI
https://doi.org/10.2991/emim-16.2016.156How to use a DOI?
Open Access
This is an open access article distributed under the CC BY-NC license.

Cite this article

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  - 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  - https://doi.org/10.2991/emim-16.2016.156
ID  - Lou2016/04
ER  -