Approche d’analyse des spécifications et des conceptions de systèmes à l’aide de modèles et de propriétés vérifiables logiquement.
Hillel Wayne présente des principes issus des méthodes formelles pour détecter les défauts de conception avant l’implémentation du système, en mettant l’accent sur la force des propriétés, l’exploration de l’espace des états et les hypothèses relatives à l’environnement. Les exemples montrent comment une analyse simplifiée de la concurrence, des défaillances et des nouvelles tentatives peut révéler tôt des erreurs coûteuses.