A three-level verification approach on Wireless Communication Controller System

Wireless Communication Controller System is an industrial communication system that controls multiple categories of radios to communicate with remote systems. Due to high cost and great uncertainty in this wireless system test, we present our work in terms of formally modeling, verifying and improving the system. To deal with the complexity of concurrent system verification, we propose a three-level verification method, from the lowest function view to secondary component view and then to the highest system view. By SPIN model checker, we have discovered some deadlock scenarios and boundary-value errors in the system. After being corrected, the system demonstrates well behaviors in the next step of verification.