Técnicas de Descripción Formal

Técnicas de Descripción Formal

Los métodos de especificación formal, son métodos formales dedicados a escribir especificaciones de sistemas. La mayor parte de los métodos de especificación formal son notaciones que permiten especificar y razonar sobre el comportamiento de sistemas. Esta característica hace necesaria la experiencia y adecuada formación del equipo de desarrollo para trabajar con abstracciones y modelos de sistemas.[DUQUE 2000]
Una especificación formal es una expresión matemática que contiene la descripción de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008]
En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de la calidad del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad.
Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]:
En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes.
En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado.
En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática.

Verificación Formal

Las TDF contribuyen a reducir el riesgo inherente a la fase de captura y especificación de requisitos del sistema. No obstante, es importante ser consciente de que una especificación de un sistema escrita en una notación formal puede contener también errores. Para aumentar la confianza del diseñador en la corrección del método es preciso realizar operaciones de verificación sobre la especificación. Muchas veces esta verificación se realiza de manera informal a través de inspecciones y reuniones de revisión. Sin embargo, la base matemática de los métodos de especificación formal posibilita la verificación formal en dos aspectos: verificación formal de propiedades formuladas sobre la especificación, y verificación formal de que la implementación satisface la especificación.[DUQUE 2000]
Una de las más importantes motivaciones que impulsó el desarrollo de las TDF fue la posibilidad de realizar una verificación formal del sistema obtenido. No obstante, es en este último punto donde surgen más controversias sobre la utilidad de las mismas. Por una parte, la experiencia ha demostrado que la verificación formal de grandes especificaciones es, en muchos casos, inviable por el alto coste de recursos que es necesario invertir. Por lo que entonces es necesario limitar o concentrar las verificaciones a partes del sistema que por su naturaleza se consideren más críticas.
Un método alternativo [DUQUE 2000] a la verificación formal citada –verificación formal de que la implementación satisface la especificación-, lo constituye un proceso de refinamiento iterativo donde la especificación formal de un sistema se obtiene tras la aplicación sucesiva de un conjunto de simples refinamientos o transformaciones aplicadas a una especificación inicial del sistema con un elevado nivel de abstracción. Cada una de las fases de este proceso toma como entrada la especificación resultante del refinamiento anterior y produce como salida otra especificación con mayor cantidad de detalles de implementación. Éste proceso continúa hasta que se dispone de una especificación con el nivel de detalle suficiente como para poder traducirla a un lenguaje de programación convencional. Las especificaciones de entrada y salida de un refinamiento se pueden relacionar mediante relaciones de equivalencia o de orden. Las ventajas, a priori, de este método es que las verificaciones que se hacen son mucho más simples.

Referencias

DUQUE, J. G. Especificación, verificación y mantenimiento de requisitos funcionales con técnicas de descripción formal. España, Universidad de Vigo, Departamento de Tecnologías de las Comunicaciones, ETSI de Telecomunicación, 2000. p.

MUÑOZ, C. “Métodos Formales, por ejemplo” Computer Science Laboratory, SRI International. En sitio: “NIA: National Institute of Aerospace”
Publicado: 1998. , 1998. [Disponible en: Disponible en:
<http://www.csl.sri.com/users/munoz/Papers/mfhtml/mfhtml.html >