A method of automatic formulation by a computer of test cases for verifying at least one function of a piece of software in relation to a specification including requirements relating input values and output values of the software, the method including the steps of: distinguishing combinatorial requirements and sequential requirements; modeling combinatorial requirements by a truth table and sequential requirements by a finite state machine to obtain a modeled specification; establishing an operation matrix relating the input values of the software with a probability of them being in succession and a transition time between them; selecting the successions of input values to be tested by performing a Monte Carlo draw on the operation matrix; determining a test case including test rows relating each selected succession with the output values expected given the modeled specification; stopping the determination process when the test case being determined makes it possible to reach a predetermined threshold for at least one of the following criteria: verified percentage of function code, verified percentage of requirements, verification time, and verification cost.