6. Conclusion
Le champ des méthodes formelles est foisonnant. De très nombreux travaux de recherche ont contribué à l'émergence d'une palette variée de méthodes différentes, chacune adaptée pour traiter un aspect particulier de la vérification. Certaines propositions académiques ont abouti à des transformations industrielles réussies : le model-checking par BDD et SAT est totalement intégré dans le flot de conception des fabricants de logiciels d'aide à la conception de circuits (CAD). L'analyse de logiciel par interprétation abstraite ou les méthodes de modélisation – vérification – production de code ou circuits issus des travaux sur les langages synchrones sont utilisées couramment dans l'industrie aéronautique. La méthode B est utilisée dans le domaine ferroviaire. La preuve assistée a été mise en œuvre pour certifier des compilateurs extrêmement complexes et est intégrée au flot...
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Conclusion
Sources bibliographiques
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Article inclus dans l'offre
"Technologies logicielles Architectures des systèmes"
(
408 articles
)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
