Bajo el título Especificación de los Sistemas Software se presentan diversas metodologías y técnicas formales para especificar requisitos en distintas etapas del proceso de desarrollo de sistemas software.
    La especificación de los requisitos ya sea de un sistema software entero, o la de algún componente o módulo del diseño, es una tarea crucial en el proceso de desarrollo del  mismo, ya que este conjunto de especificaciones indica su funcionalidad (del sistema o módulo) y por tanto servirán para validarlo y verificarlo.
    En determinadas situaciones, cuando el sistema se vuelve complejo por diversos motivos: tamaño, fuertes restricciones de seguridad, transacciones bancarias, etc, su correcto funcionamiento se vuelve una cuestión crítica. Es en este contexto cuando aparece la necesidad de poder expresar los requisitos mediante métodos formales que nos garanticen el correcto funcionamiento del sistema. Con estos métodos formales de especificación se dispone de una herramienta capaz de verificar y validar los requisitos mediante procedimientos mecánicos; quitando así posibles ambigüedades y errores provenientes de una mala comprensión del funcionamiento del sistema.
    Estas técnicas o sistemas formales constan de un lenguaje formal y un sistema de deducción. Cada uno de estos sistemas formales utiliza un determinado formalismo matemático. Veremos algunos de ellos como: Z, VDM y sobre todo ALLOY.