Quindi con Model Checking hai una specifica e il checker del modello passa automaticamente attraverso gli stati del tuo programma e controlla se corrisponde alle specifiche. Quello che non capisco è dove il test si adatta. Pertanto, in genere viene descritto che se Model Checking rileva un errore, genererà un test case per dimostrare l'errore. Questo ha senso, questo ti permette di scorrere su una soluzione fino alla fine del test.
La mia prima domanda è, supponendo che tu faccia passare quel test (il test generato dal correttore del modello), mi chiedo cosa tu fai con il test:
- Buttalo via, non è più necessario.
- Salvalo per testare periodicamente in un'esecuzione di test di regressione. (Ma sembra che il controllore del modello lo catturerà comunque, quindi non sono sicuro che sia necessario, sembra una duplicazione.)
- In qualche modo hanno una serie di test accanto al correttore / specifica del modello che si esegue sempre perché il controllore del modello non può gestirli.
Questo fa apparire la seconda parte della domanda che è, il tipo di cose per cui scrivi i test se hai il model checking. Se questo è troppo ampio, sarebbe utile solo conoscere il flusso di lavoro per affrontare i test generati dal modello di verifica.