Generation of functional test sequences from B formal specifications presentation and industrial case-study

The paper presents an original method to generate test sequences. From formal specifications of the system to be tested, an equivalent system of constraints is derived, and then the domain of each state variable of this system is partitioned into subdomains. Using this partition, limit states are computed with a specific solver that uses constraint logic programming with sets. This specific solver is then used to build test sequences by traversing the constrained reachability graph of the specifications. Finally, the formal specifications are used as an oracle by using them to determine the expected output for a given input. The results of an industrial case-study of the Smart Card GSM 11-11 standard are presented and discussed.