Estos involucran una serie de técnicas lógicas y matemáticas con la que es posible especificar, diseñar, implementar y verificar los sistemas de información. [1]
Desde hace varias décadas se utilizan técnicas de notación formal para modelar los requisitos, principalmente porque estas notaciones se pueden verificar fácilmente y porque, de cierta forma, son más comprensibles para el usuario final [2] . Además, el paradigma Orientado a Objetos en la programación parece ser el mas utilizado en la industria y una forma de incrementar la confiabilidad del software y en general de los sistemas, es utilizar los métodos formales en la ingeniería aplicada.[3]
El termino métodos formales se refiere entonces al use de técnicas de la lógica y de la matemática discreta para especificar, diseñar, verificar, desarrollar y validar programas.
La palabra formal se deriva de la lógica formal, ciencia que estudia el razonamiento desde el análisis formal de acuerdo con su validez o no validez y omite el contenido empírico del razonamiento para considerar solo la forma estructura sin materia. Los métodos formales más rigurosos aplican estas técnicas para comprobar los argumentos utilizados para justificar los requisitos, u otros aspectos de diseño e implementación de un sistema complejo.
En la lógica formal como en los métodos formales el objetivo es el mismo, “reducir la dependencia de la intuición y el juicio humano para evaluar argumentos”[4]
Un método formal si posee una base matemática estable, normalmente soportada por un lenguaje de especificación formal, que permite definir de manera precisa nociones como consistencia y completitud y aun mas relevantes la especificación la implementación y la correctitud. Al utilizar notaciones y lenguajes formales es posible estructurar claramente los requisitos del sistema y general las especificaciones que permitan definir su comportamiento de acuerdo con el “que debe hacer” y no con el “como lo hace”.
