Mi piace scrivere test delle unità quando creo software. Recentemente ho imparato a conoscere il Model Checking per dimostrare che un sistema corrisponde a una specifica. Ora sto tornando a test per vedere se ha qualche utilità al fianco di Model Checking. In particolare, sono interessato alla generazione di test case, che Model Checking sembra supportare.
La mia domanda è, in che modo la generazione di test automatizzata funziona ad alto livello / flusso di lavoro. Nel caso di Model Checking, se passa solo attraverso lo spazio degli stati, trova qualcosa che non funziona, e quindi in qualche modo scopre di generare alcuni input arbitrari per dimostrare l'errore. Allora mi chiedo cosa farai con questi test. Se vengono salvati in una cartella "suite di test generata automaticamente" nell'applicazione, o vengono semplicemente creati dinamicamente al volo. Sembra che potresti volerli raccogliere mentre vai per evitare regressioni. Quindi, chiedendo se questi test vengono eseguiti manualmente in modo simile ai test delle unità, o se si tratta di qualcosa come il Model Checker per gestirli / archiviarli / eseguirli se necessario. Chiedendosi inoltre come il generatore di test calcoli quali valori inserire in qualsiasi situazione. Forse ci sono alcune euristiche o database di input di esempio da qualche parte, in pratica quello che mi chiedo, come gestirlo in pratica.