Los métodos de prueba basados en especificaciones generan datos de prueba sin el conocimiento de la estructura del programa. Sin embargo, la calidad de estos datos de prueba no está bien asegurada para detectar errores cuando se introducen cambios no funcionales en el programa. Para generar datos de prueba de manera efectiva, proponemos un nuevo método que combina especificaciones formales con el algoritmo genético (GA). En este método, las especificaciones formales son reformadas por GA para ser utilizadas en la generación de valores de entrada que puedan eliminar tantos mutantes del programa objetivo como sea posible. Se presentan dos ejemplos clásicos para demostrar cómo funciona el método. El resultado muestra que el método propuesto puede ayudar a generar de manera efectiva casos de prueba para eliminar los mutantes del programa, lo que contribuye al mantenimiento adicional del software.