Manque de bol, sur tes cinq examples, les trois traitants de temps de réponse sont tout à fait dans le colimateur des méthodes formelles via par exemple automates temporisés*, et du fameux problème de calcul du temps d'exécution pire cas**. En particulier, ton premier exemple est un grand classique de la vérification de système temps-réel, domaine qui me semble particulièrement bien étudié !
Pour les problèmes d'interface graphique, effectivement c'est plus difficile, et je ne pense pas que les méthodes formelles aient un quelconque intérêt.
[^] # Re: Se passer des tests ...
Posté par auve . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 6.
Pour les problèmes d'interface graphique, effectivement c'est plus difficile, et je ne pense pas que les méthodes formelles aient un quelconque intérêt.
* : http://mpri.master.univ-paris7.fr/attached-documents/C-2-8/m(...)
** : http://en.wikipedia.org/wiki/Worst-case_execution_time