Tópicos Avanzados en la Ingeniería de Software

Métodos Formales

¿Qué es? Estos métodos permiten al ingenierodel software crear una especificaciónsin ambigüedades que sea máscompleta y constante que las que seutilizan en los métodos convencionalesu orientados a objetos. La teoría deconjuntos y las notaciones lógicas seutilizan para crear una sentencia clarade hechos (o de requisitos). Esta especificación matemática entonces sepuede analizar para comprobar quesea correcta y constante. Como esta especificación se crea utilizando notaciones matemáticas. inherentementees menos ambigua que los ncdos informales de presentación.

¿Quién lo hace? Un ingeniero del softwareespecializado crea una especificación formal.

¿Por qué es imporiante? En sistemascríticos para la misión y para la seguridad,un fallo puede pagarse muycaro. Cuando la computadora falla sepueden perder vidas o incluso tenergraves consecuencias económicas. Endichas situaciones es esencial descubrirlos errores antes de poner en operaciónla computadora. Los métodosformales reducen drásticamente los errores de especificación, y consecuentemente son la base del softwareque tiene pocos errores una vez que elcliente comienza a utilizarlo.

¿Cuáles son los pasos? El primer paso en la aplicación de los métodos formaleses definir el invariante de datos, el estado y las operaciones para el funcionamiento de un sistema.El invariante de datos es una condición que se verifica mediante la ejecución de una función que contiene un conjunto de datos. Los datos almacenados forman el estado en donde una función puede acceder y alterar; y las operaciones son las acciones que tienenlugar en un sistema a medida quelee o escribe datos en un estado. Una operación se asocia a dos condiciones:una precondición y una postcondición.La notación y la heurística asociados con los conjuntos y especificaciones constructivas operadores de conjuntos, operadores lógicos y sucesiones- forman la base de losmétodos formales.

¿Cuál es el producto obtenido?Cuando se aplican métodos formalesse produce una especificación representadaen un lenguaje formal como Zo VDM.

¿Cómo puedo estar seguro de quelo he hecho corredamente? Debido a que los métodos formales utilizan la matemática discreta como mecanismo de especificación, para demostrar que una especificación es correcta,se pueden aplicar pruebas lógicas acada función del sistema