Verifying Finite State Machine Behavior using QuickCheck EQC_fsm

Abstract: In order to communicate properly, mobile telephones connect to base transceiver stations which forward the telephones’ signals. These base transceiver stations are called Node Bs. As the use of mobile telephones expands every day, the number of Node Bs in the world increases with rapid speed. This requires better software systems in the Node Bs, so people can use their mobile telephones whenever and wherever, without any obstacles in the way. Better testing tools are needed to ensure the quality of the software systems in the Node Bs. This thesis is based on the evaluation of a software testing tool called QuickCheck and especially one of its modules, eqc_fsm. The goal was to determine if the characteristics of two subsystems in Node B would make QuickCheck and its module applicable as a testing tool for those systems. Since QuickCheck can be used to test systems modeled as finite state machines, the two subsystems were modeled as numerous uniquely finite state machines and tested using QuickCheck. The systems were both successfully modeled according to eqc_fsm and tested using QuickCheck. The applicability of eqc_fsm as a testing tool was not affected to a great degree by the systems characteristics that were investigated. Eqc_fsm was also flexible to handle systems with different characteristics. This showed that QuickCheck’s eqc_fsm module was applicable as a testing tool for the two subsystems in Node B. QuickCheck and its module eqc_fsm can be used to improve the quality of the software systems in Node B.