Souvent utilisé dans le test de circuits et de logiciels informatiques, la vérification formelle est lorsque la fonction de ces systèmes est analysée en utilisant des formules mathématiques. Dans le cas du développement de logiciels, le processus est généralement utilisé pour montrer que le programme fonctionne correctement, basée sur un modèle préétabli. Parfois, le modèle théorique est avérée insatisfaisante. Outre le code source du logiciel, à la vérification formelle peut être utilisé dans le développement de circuits combinatoires, qui sont utilisés pour effectuer des calculs dans les ordinateurs, ainsi que la mémoire de l'ordinateur. Les différentes approches incluent après-coup vérification, la vérification en parallèle, et la vérification intégrée, en plus de diverses méthodes.
Procédures mathématiques pour les calculs, appelés algorithmes sont utilisés dans la vérification formelle de tester les fonctions des produits à chaque étape du développement.Les développeurs de logiciels peuvent trouver des erreurs ou des bugs à la fois dans le code source et le modèle utilisé pour le construire en premier lieu. Parfois, des changements fondamentaux dans la façon dont le code est en cours d'écriture peuvent être effectuées avant une erreur de conception affecte le résultat final. L'étape de vérification permet généralement de déterminer si le produit est en train de faire ce que l'on voulait faire, et répond aux spécifications de l'application, il est pour.
Vérification formelle peut se produire quand un produit est terminée, ce qui est appelé après-coup vérification. Une méthode standard, utilisé tout au long du processus de conception et de développement, n'est pas analysée jusqu'à ce que le système est terminée. Localisation de graves erreurs à ce stade conduit souvent à des révisions coûteuses et de longue haleine. Le développement et la vérification peuvent également être effectuées par deux équipes distinctes pour la vérification en parallèle. Grâce intercommunication, les développeurs peuvent se concentrer sur des tâches indépendantes durant tout le processus de conception.
Vérification intégrée est quand une équipe effectue la mise au point et l'évaluation requise.Concepts mathématiques complexes sont souvent utilisés pour vérifier les capacités du produit le long du chemin. Les méthodes de vérification formelle varient selon les projets, mais on a souvent utilisé est le model checking. Un modèle de logiciel ou de matériel se compose de diverses propriétés que les concepteurs veulent dans le produit fini. Le modèle et le système peuvent être vérifiés périodiquement pour voir si les propriétés correspondent.
Une autre technique de vérification formelle consiste à utiliser des formules mathématiques et de la logique pour représenter un système et ses propriétés. Règles définies dans un système formel sont généralement trouvés dans la logique. Ces deux techniques utilisent divers moyens pour déterminer si une spécification particulière d'un produit est atteint. Les développeurs peuvent utiliser différents types de logiciels dans le processus de vérification formelle, chacun adapté à un système spécifique ou langage de programmation
