Métodos formales e Ingeniería de Software

4. Ventajas de los métodos formales

La utilidad de los métodos formales en la Ingeniería de Software es un tema que
se debate desde hace varias décadas. Recientemente, con el surgimiento de la
Ingeniería de Conocimiento en la Sociedad de la Información, y la aplicación de los
métodos formales en los procesos industriales, nuevamente surge el debate.

A continuación se detallan algunas de las ventajas de utilizarlos.

Especificación. Uno de los problemas más ampliamente reconocido en el
desarrollo de software es la dificultad para especificar claramente el
comportamiento que se espera del software, problema que se agudiza con el
actual desarrollo basado en componentes, ya que el ingeniero tiene sólo una
descripción textual de los requisitos, procedimientos, entradas permitidas y
salidas esperadas. Asegurar que este tipo de software sea seguro es un problema,
no sólo por su tamaño y complejidad, sino porque el código fuente no suele estar
disponible para los componentes que se adquieren. Una forma de ofrecer
“garantía rigurosa” del producto es definir, con precisión, el comportamiento
esperado del software (NASA, 1995). La especificación formal proporciona mayor
precisión en el desarrollo de software, y los métodos formales brindan las
herramientas que pueden incrementar la garantía buscada. Desarrollar
formalmente una especificación requiere conocimiento detallado y preciso del
sistema, lo que ayuda a exponer errores y omisiones, y por lo que la mayor
ventaja de los métodos formales se da en el desarrollo de la especificación (Clarke
& Wing, 1996). En la formalización de la descripción del sistema se detectan
ambigüedades y omisiones, y una especificación formal puede mejorar la
comunicación entre ingenieros y clientes. Los métodos formales se desarrollaron
principalmente para permitir un mejor razonamiento acerca de los sistemas y el
software. Luego de diseñar una especificación formal, se puede analizar,
manipular y razonar sobre ella, de la misma forma que sobre cualquiera expresión
matemática. Una diferencia significativa entre una especificación formal de
software y una expresión matemática de álgebra o cálculo, es que típicamente es
mucho más grande -a menudo cientos o miles de líneas-. Para tratar con el
tamaño y la complejidad de estas expresiones se desarrollan herramientas de
software que se pueden agrupar en dos grandes categorías: probadoras de
teoremas y verificadoras de modelos (Anderson et al, 1998). Las primeras ayudan
al usuario a diseñar pruebas, generalmente para demostrar que las
especificaciones cumplen con las propiedades deseadas. Para usarlas, es
necesario que el ingeniero tenga cierto grado de habilidad y conocimiento, pero
pueden manipular especificaciones muy grandes con propiedades complejas. Los
desarrollos recientes en métodos formales introdujeron las verificadoras de
modelos, que exploran, hasta cierto punto, todas las posibles ejecuciones del
programa especificado. Pueden verificar si cumple con una propiedad específica
mediante la exploración de todas las posibles ejecuciones, o producen
contraejemplos en los que la propiedad no se cumple. Aunque estas herramientas
pueden ser completamente automáticas, no pueden resolver problemas tan
grandes o variados como las probadoras de teoremas. Las herramientas más
sofisticadas combinan aspectos de ambas, aplican las verificadoras a algunas
partes de la especificación, pero confían en el usuario para probar las propiedades
complicadas.

Verificación. Para asegurar la calidad de los sistemas es necesario probarlos, y

para asegurar que se desarrollan pruebas rigurosas se requiere una precisa y
completa descripción de sus funciones, incluso cuando en la especificación se
utilicen métodos formales. Una de las aplicaciones más interesantes de éstos es el
desarrollo de herramientas, que pueden generar casos de prueba completos
desde la especificación formal. Aunque gran número de herramientas para
automatizar pruebas se encuentran disponibles en el mercado, la mayoría
automatiza sólo sus aspectos más simples: generan los datos de prueba, ingresan
esos datos al sistema y reportan resultados. Definir la respuesta correcta del
sistema, para un determinado conjunto de datos de entrada, es una tarea ardua,
que la mayoría de herramientas no puede lograr cuando el comportamiento del
mismo se especifica en lenguaje natural. Debido a que la respuesta esperada del
sistema se puede determinar únicamente mediante la lectura de la especificación,
los ingenieros esperan que a las pruebas automatizadas se les adicione este
faltante y crítico componente (Dan & Aichernig, 2002). La gran ventaja de las
herramientas, que generan pruebas con base en los métodos formales, es que la
especificación formal describe matemáticamente el comportamiento del sistema,
desde la que se puede generar la respuesta a un dato de entrada en particular, es
decir, la herramienta puede generar casos de prueba completos. Las técnicas de
verificación formal dependen de especificaciones matemáticamente precisas y,
desde un punto de vista costo-beneficio, generar pruebas desde la especificación
puede ser uno de los usos más productivos de los métodos formales.
Aproximadamente la mitad del tiempo del equipo de trabajo, en un desarrollo
típico de software comercial, se invierte en esfuerzo para desarrollar pruebas, e
“incluso con este nivel de esfuerzo sólo se eliminan los errores más evidentes”
(Saiedian & Hinchey, 1996). Algunas mediciones empíricas demuestran que las
pruebas, generadas con herramientas automatizadas, ofrecen una cobertura tan
buena o mejor que la alcanzada por las manuales, por lo que los ingenieros
pueden elegir entre producir más pruebas en el mismo tiempo, o reducir el
número de horas necesarias para hacerlas (Gabbar, 2006).

Validación. Mientras que la verificación se puede realizar semiautomáticamente y

las pruebas mecánicamente, la validación es un problema diferente. Una
diferencia específica entre verificación y validación es que la primera responde a
si “se está construyendo el producto correctamente”, y la segunda a si "se está
construyendo el producto correcto" (Dasso & Funes, 2007). En otras palabras, la
verificación es el conjunto de actividades que aseguran que el software
implementa correctamente una función específica, y la validación es un conjunto
de actividades diferentes que aseguran que el software construido corresponde
con los requisitos del cliente (Amman & Offutt, 2008). Desde el conjunto de
requisitos es posible verificar, formal o informalmente, si el sistema los
implementa; sin embargo, la validación es necesariamente un proceso informal.
Sólo el juicio humano puede determinar si el sistema que se especificó y
desarrolló es el adecuado para el trabajo. A pesar de la necesidad de utilizar este
juicio en el proceso de validación, los métodos formales tienen su lugar,
especialmente en grandes y complejas aplicaciones, como en modelado y
simulación. Una de sus aplicaciones más prometedoras es en el modelado de
requisitos, ya que, al diseñarlos formalmente, el teorema provisto en la
herramienta de prueba se puede utilizar para explorar sus propiedades, y a
menudo detectar los conflictos entre ellos. Este método no sustituye al juicio
humano, pero puede ayudar a determinar si se especificó el "sistema correcto",
por lo que es más fácil determinar si las propiedades deseadas se mantienen
(Flynn & Hamlet, 2006). Una diferencia significativa entre validar sistemas de
modelado y simulación, y los de control o cálculo, es que los primeros tienen dos
tipos de requisitos de validación: deben modelar y predecir el comportamiento de
alguna entidad del mundo real, problema que se conoce como "validación
operacional", y deben "validar el modelo conceptual", para asegurar que la
hipótesis en la que se sustenta es correcta, y que su lógica y estructura son
adecuadas para el modelo que se propone (Sargent, 1999). Debido a que el
modelo conceptual describe lo que debe representar la simulación, es necesario
incluir supuestos acerca del sistema, su entorno, las ecuaciones, los algoritmos,
los datos, y de las relaciones entre las entidades del modelo. Aunque los
algoritmos y las ecuaciones son declaraciones necesariamente formales, los
supuestos y las relaciones se describen normalmente en lenguaje natural, lo que
introduce potenciales ambigüedades e incomprensiones entre ingenieros y
usuarios. Una tendencia relativamente reciente en los métodos formales,
conocida como "métodos formales ligeros" (Jackson, 2001), demuestra tener
potencial para detectar errores importantes en la declaración de requisitos, sin el
costo de una verificación diseñada formalmente. La premisa básica de este
enfoque es el uso de técnicas formales en el análisis de los supuestos, las
relaciones y las propiedades de los requisitos, indicadas en su declaración o en el
modelo conceptual. Se puede aplicar a especificaciones parciales o a un segmento
de la especificación completa, proceso que se realiza en tres fases: 1) reafirmar
los requisitos y el modelo conceptual en una notación formal -o semiformal-,
típicamente en una tabla de descripción de estados; 2) identificar y corregir las
ambigüedades, conflictos e inconsistencias; y 3) utilizar un verificador de modelos
o un probador de teoremas para estudiar el comportamiento del sistema,
demostrar sus propiedades y graficar su comportamiento. Los ingenieros y
usuarios pueden utilizar estos resultados para mejorar el modelo conceptual
(Davis, 2005). Un aspecto particularmente interesante de este enfoque es que se
ha utilizado para modelar y analizar el comportamiento del software, del
hardware y de las acciones humanas en los sistemas (Mazzola et al, 2006).
Agerholm y Larsen (1997) describen su aplicación en un sistema de actividad
extra-vehicular de la NASA; y Lutz (1997) describe la validación de requisitos de
los monitores de errores a bordo de una nave espacial. Un detalle importante de
este proyecto es que los ingenieros utilizaron el modelo de requisitos para un
segundo proyecto, que se desarrolló a partir del primero, como una construcción
en serie. Janssen et al (1999) describen la aplicación de un verificador de modelos
para analizar procesos de negocios automatizados, como el procesamiento de
reclamaciones de seguros.

5. El futuro de los métodos formales

La industria del software tiene una larga y bien ganada reputación de no cumplir
sus promesas y, a pesar de más de 60 años de progreso, tiene años -incluso
décadas- por debajo de la madurez necesaria que requiere para satisfacer las
necesidades de la naciente Sociedad del Conocimiento. Goguen (1997) cita
algunas estimaciones de los gastos que generan los fracasos del desarrollo de
software, los calculó en 81 mil millones de dólares para 1995 y en 100 mil
millones para 1996; posteriormente (1999), llamaba la atención sobre la
cancelación del contrato de 8 mil millones de dólares a The International Business
Machines -IBM- por la FAA -The Federal Aviation Administration-, para el diseño
de un sistema de control aéreo para toda la nación; y del contrato del DOD -
United States Department of Defense-, a la misma IBM, por $2 mil millones para
modernizar su sistema de información; del fallo del software para la entrega en
tiempo real de datos en las Olimpiadas de 1996; y del año y medio de retraso en
el sistema para el manejo automatizado de equipaje en el aeropuerto de Denver
para United Airlines, con un costo de $1,1 millones diarios. En su libro, Neumann
(1994) revela que estos problemas no son en absoluto nuevos, aunque parece
que se incrementan; incluso señala que algunos de ellos ya provocaron muertes
de personas, por ejemplo la sobredosis de radiación en un sistema de terapia a
mediados de los 80 (Gowen & Yap, 1991). Es claro que aún no es posible, con la
tecnología actual, asegurar el éxito de los proyectos de software, y que para
proyectos grandes y complejos el enfoque ad hoc ha demostrado ser insuficiente.
La falta de formalización en los puntos clave de la Ingeniería de Software la hace
sensible a problemas que son inevitables en actividades altamente técnicas y
detalladas como la creación de software. Las buenas prácticas en Ingeniería
deben aplicarse en todo el proceso del desarrollo de sistemas, pero, aunque el
desarrollo tecnológico aporta mucho material para alcanzarlo, todavía no se logra
este objetivo. Incrementar la precisión y el control riguroso es esencial, y es el
principal objetivo de los métodos formales, que utilizan esencialmente
formalismos lógicos buscando mejorar el software y el hardware, en áreas como
confiabilidad, seguridad, productividad y reutilización. Los ejes principales de su
accionar son la verificación del código y el diseño, así como la generación de
programas y casos de prueba desde las especificaciones. Los métodos formales
deberían estar presentes como principios esenciales de las técnicas de prueba.
Gaudel (1995) lo estableció como un tema importante de investigación; Hoare
(2002a) describió el uso de aserciones formales no para probar el programa, sino
para diseñar las pruebas; y Hierons et al. (2008) desarrollaron una investigación
en aspectos formales de las pruebas. Los métodos formales se utilizan en el
mantenimiento del software (Younger et al., 1996) y en su evolución (Ward &
Bennett, 1995), y tal vez su más amplia aplicación sea en el mantenimiento de
código heredado (Hoare, 2002b). Los métodos formales son un área de
investigación muy activa, y se espera que cada día se incrementen las
colaboraciones. Existen varias revistas especializadas, como Formal Aspects of
Computing y Formal Methods in System Design, que hacen hincapié en sus
aplicaciones prácticas, así como en la teoría. Conferencias como la NASA Formal
Methods Symposium y la Computer-Aided Verification están dedicadas al tema y
tienen procesos de selección de aportes muy competitivos. Otras conferencias
importantes son Principles of Programming Languages, Logic in Computer
Science, y Conference on Automated Deduction. Existen talleres y conferencias
especializadas más pequeñas, algunas enfocadas en herramientas y técnicas,
como la ABZ, que cubre las notaciones Alloy, ASM, B y Z, y talleres de
refinamiento. Unas debaten cuestiones teóricas específicas, como Integrated
Formal Methods, y otras cubren áreas de aplicación, como Formal Methods for
Open Object-based Distributed Systems y Formal Methods for Human-Computer
Interaction. The Computer Science Bibliography ([Link]-
[Link]/~ley/db/, enero 2010) contiene referencias a más de un millón de
artículos, indexados por metadatos, entre los que existen gran cantidad acerca de
los métodos formales, especificación, verificación y validación, muchos de edición
reciente, lo que presupone que para esta área la producción está en incremento.
Se estima que en [Link]. existen por lo menos 1.000 investigadores en
verificación, cerca de 300 profesores y 200 estudiantes graduados de pregrado, y
alrededor de 250 investigadores en la industria –Microsoft, Intel, Cisco, IBM,
Cadence, Synopsys, Mentor Graphics-, y 50 en el gobierno – NASA, NSA, NRL–
(Woodcock et al, 2009). The UK Engineering and Physical Science Research
Council desarrolla por lo menos 400 proyectos de investigación en Ingeniería de
Software, y The Fundamentals of Computing dedica US $144 millones a
patrocinios. Además, se estima que en Europa existen más de 1.000
investigadores, en China 250, en los países bajos 500, en Australia, Brasil, Canadá,
Nueva Zelanda y África, unos 1.000. Se espera que una pesquisa futura -por lo
menos en 10 años-, y de acuerdo con las proyecciones aquí mostradas, demuestre
un notable incremento en investigación, desarrollo y aplicación; y entonces será
posible una mayor aceptación en la industria, mayor participación de las
facultades de Ingeniería y la academia en general, y más trabajo práctico y
experimental alrededor de los métodos formales. Con esto se podrá concretar el
apoyo decidido a la visión de Hoare (2003, 2007) de “un mundo en el que los
productos software siempre serán fiables, y que la labor de los ingenieros de
software sea realmente Ingeniería”.

6. Conclusiones
 Los métodos formales son técnicas matemáticas, a menudo soportadas por
herramientas, para el desarrollo de sistemas software y hardware. Su rigor
matemático le permite a los ingenieros analizar y verificar sus modelos en
cualquier parte del ciclo de vida del desarrollo; y dado que la fase más importante
en estos procesos es la Ingeniería de Requisitos, son útiles para elicitarlos,
articularlos, representarlos y especificarlos (George & Vaughn, 2003). Sus
herramientas proporcionan el soporte automatizado necesario para la integridad,
trazabilidad, verificabilidad, reutilización, y para apoyar la evolución de los
requisitos, los puntos de vista diversos y la gestión de las inconsistencias (Ghose,
2000).  Los métodos formales se utilizan en la especificación de software, y se
emplean para desarrollar una declaración precisa de lo que el software tiene que
hacer, evitando al mismo tiempo las restricciones del cómo se quiere lograr. La
especificación es un contrato técnico entre el ingeniero y el cliente, que
proporciona un entendimiento común de la finalidad del software; el cliente la
utiliza para orientar la aplicación del software, y el ingeniero para guiar su
construcción. Una especificación compleja se puede descomponer en sub-
especificaciones, que describen un subcomponente del sistema que se pueden
delegar a otros ingenieros - diseño por contrato- (Meyer & Mandrioli, 1992).
 Los sistemas de software complejos requieren una cuidadosa organización de la
estructura arquitectónica de sus componentes, un modelo del sistema que
suprima detalles de la implementación, y que permita al arquitecto concentrarse
en los análisis y decisiones más importantes para estructurar el sistema y
satisfacer sus requisitos (Allen & Garlan, 1992), (Lamsweerde, 2003). Darwin
(Magee & Kramer, 1996) y Wright (Allen, 1997) son ejemplos de lenguajes de
descripción arquitectónica basados en la formalización del comportamiento
abstracto de los componentes y conectores arquitectónicos.
 Los métodos formales se utilizan en el diseño de software, donde el
refinamiento de datos incluye la especificación de máquinas de estado, funciones
de abstracción y pruebas de simulación (Hoare, 1975); cumplen un rol
protagónico en métodos como VDM y Z, y en el cálculo de refinamiento de
programas (Dijkstra, 1975).
 En la fase de implementación, los métodos formales se utilizan para verificar el
código, ya que toda especificación tiene explícito un teorema de correctitud con
el que, si se cumplen ciertas condiciones, el programa deberá conseguir el
resultado descrito en la documentación. La verificación del código es un intento
por demostrar este teorema, o al menos de encontrar por qué falla. El método de
verificación por aserción inductiva de programas fue desarrollado por Floyd
(1967) y Hoare (1969), y consiste en anotar el programa con aserciones
matemáticas, o sea las relaciones entre las variables y los valores iniciales de
entrada.
 Más de cuatro décadas de investigación y experimentación demostraron que
los métodos formales son, hasta el momento, el único medio práctico para
exponer la ausencia de comportamientos no deseados en los programas, una
propiedad esencial en los sistemas críticos. Los modelos para probar calidad
industrial, y los probadores de teoremas avanzados permiten, de forma
automática o semiautomática, hacer análisis complejos de las especificaciones
formales, por lo que estas herramientas son atractivas para uso comercial.
 La capacidad para generar casos de prueba completos desde la especificación
formal, representa un ahorro sustancial a pesar del costo de su desarrollo. La
experiencia demuestra que las técnicas formales se pueden aplicar
productivamente, incluso en las pruebas más completas. El proceso para
desarrollar una especificación es la fase más importante de la verificación formal,
y el enfoque de los "métodos formales ligeros" permite analizar formalmente las
especificaciones parciales, y la definición temprana de requisitos.