Formal Verification of Serial Port Module in Robot Control System
Chenhui Lou, Xiaojuan Li
Available Online April 2016.
- https://doi.org/10.2991/emim-16.2016.156How to use a DOI?
- Robot control system; Serial module; Formal verification; Theorem proving
- 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.
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 -