Buscar este blog

jueves, 24 de febrero de 2011

Especificacion formal

Introduccion
La calidad del software es una de las problematicas mas importantes en los procesos de desarrollo de software. Garantizar el correcto funcionamiento bajo situaciones no determinadas es una tarea que tiene que ser realizada con cuidado extremo. En algunos casos, este tipo de pruebas son de mayor importancia, ya que involucran ambientes sensibles e informacion critica en donde es necesario garantizar que cada uno de los componentes involucrados (hardware, software y componentes humanos) actue de manera correcta ante situaciones especificas, con una variedad de ejemplos que cubren areas tan diversas como planeacion de trafico, aplicaciones militares y sistemas medicos, entre muchas otras.
Los modelos formales presentan una alternativa practica para solucionar estos problemas. Constituyen un enfoque analitico para la especificacion, diseño y verificacion de sistemas de hardware y software. Su caracteristica principal es la rigurosidad en la que sus modelos se encuentran basados, con fundamentos en solidos principios matematicos que permiten definir con precision y sin temor a ambiguedades las necesidades de un sistema. Gracias a estos fundamentos, el software generado mediante metodos formales puede ser verificado mediante el cumplimiento de propiedades derivadas de la especificacion. Este enfoque ha resultado ser exitoso frente a otras tendencias, encontrando errores en diseño que dificilmente habrian podido ser considerados usando otras tecnicas.
Definiciones: Metodos Formales
Una de las metas de la Ingenieria del Software es lograr que los desarrolladores construyan sistemas confiables independientemente de su complejidad. Una forma de alcanzar esta meta es a través del uso de Métodos Formales (MF): técnicas, lenguajes y herramientas definidos matemáticamente, para especificar y verificar tales sistemas. El uso de MF propicia la confiabilidad y la seguridad de un sistema, al aumentar la comprensión acerca de un sistema revelando inconsistencias, ambigüedades e incompletitudes, que de otra manera pasan desapercibidas. [L. Mendoza, M. Pérez y M. Capel]
Los métodos formales que se utilizan para desarrollar sistemas de computadoras son técnicas de base matemática para describir las propiedades del sistema. Estos métodos formales proporcionan marcos de referencia en el seno de los cuales las personas pueden especificar, desarrollar y verificar los sistemas de manera sistemática, en lugar de hacerlo ad hoc. [John J. Marciniak]
Los metodos formales representan un conjunto de tendencias de desarrollo de software y hardware en donde la especificacion, verificacion y diseño de componentes se realiza mediante notaciones, lenguajes, herramientas y tecnicas basadas en teorias con solida fundamentacion matematica. El uso de notaciones y lenguajes formales permite plantear de manera clara los requerimientos de un sistema, generando especificaciones que definen el comportamiento en terminos del “que debe hacer” y no del “como lo hace”. [Hugo A. Lopez A.]
Los metodos formales permiten al ingeniero del software crear una especificación sin ambigüedades que sea más completa y constante que las que se utilizan en los métodos convencionales u orientados a objetos. La teoría de conjuntos y las notaciones lógicas se utilizan para crear una sentencia clara de hechos (o de requisitos). Esta especificación matemática entonces se puede analizar para comprobar que sea correcta y constante. Como esta especificación se crea utilizando notaciones matemáticas inherentemente es menos ambigua que los nodos informales de presentación. [Roger Pressman]
En Ingenieria del Software un método formal es un camino a la construcción y análisis de modelos matemáticos que permitan una automatización del desarrollo de sistemas informáticos. Los métodos formales se caracterizan por emplear técnicas y herramientas matemáticas para lograr una facilitación a la hora de encarar la construcción o el análisis de un modelo matemático de un sistema. [Wikipedia]
Los diez mandamientos de los metodos formales
La decisión de hacer uso de los métodos formales en el mundo real no debe de adoptarse a la ligera. Bowen y Hinchley  han acuñado los diez mandamientos de los métodos formales, como guía para aquellos que estén a punto de embarcarse en este importante enfoque de la Ingenieria del Software.
  1. Seleccionarás la notación adecuada. Con objeto de seleccionar eficientemente dentro de la amplia gama de lenguajes de especificación formal existente, el ingeniero del software deberá considerar el vocabulario del lenguaje, el tipo de aplicación que haya que especificar y el grado de utilización del lenguaje.
  2. Formalizarás, pero no de más. En general, resulta necesario aplicar los métodos formales a todos los aspectos de los sistemas de cierta envergadura. Aquellos componentes que sean críticos para la seguridad serán nuestras primeras opciones, e irán seguidos por aquellos componentes cuyo fallo no se pueda admitir (por razones de negocios).
  3. Estimarás los costes. Los métodos formales tienen unos costes de arranque considerables. El entrenamiento del personal, la adquisición de herramientas de apoyo y la utilización de asesores bajo contrato dan lugar a unos costes elevados en la primera ocasión. Estos costes deben tenerse en cuenta cuando se esté considerando el beneficio obtenido frente a esa inversión asociada a los métodos formales.
  4. Poseerás un experto en métodos formales a tu disposición. El entrenamiento de expertos y la asesoría continua son esenciales para el éxito cuando se utilizan los métodos formales por primera vez.
  5. No abandonarás tus métodos formales de desarrollo. Es posible, y en muchos casos resulta deseable, integrar los métodos formales con los métodos convencionales y/o con métodos orientados a objetos. Cada uno de estos métodos posee sus ventajas y sus inconvenientes. Una combinación de ambos, aplicada de forma adecuada, puede producir excelentes resultados.
  6. Documentarás suficientemente. Los métodos formales proporcionan un método conciso, sin ambigüedades y consistente para documentar los requisitos del sistema. Sin embargo, se recomienda que se adjunte un comentario en lenguaje natural a la especificación formal, para que sirva como mecanismo para reforzar la comprensión del sistema por parte de los lectores.
  7. No comprometerás los estándares de calidad. Los métodos formales no tienen nada de mágico, y por esta razón, las demás actividades de SQA deben de seguir aplicándose cuando se desarrollen sistemas.
  8. No serás dogmático. El ingeniero de software debe reconocer que los métodos formales no son una garantía de corrección. Es posible (o como algunos probablemente dirían) que el sistema final, aun cuando se haya desarrollado empleando métodos formales, siga conteniendo pequeñas omisiones, errores de menor importancia y otros atributos que no satisfagan nuestras expectativas.
  9. Comprobarás, comprobarás y volverás a comprobar. Los métodos formales no absuelven al ingeniero del software de la necesidad de llevar a cabo unas comprobaciones exhaustivas y bien planeadas.
  10. Reutilizarás cuanto puedas. A la larga, la única forma racional de reducir los costes del software y de incrementar la calidad del software pasa por la reutilización. Los métodos formales no modifican esta realidad. De hecho, quizás suceda que los métodos formales sean un enfoque adecuado cuando es preciso crear componentes para bibliotecas reutilizables.
Los siete mitos sobre los metodos formales
Los siete mitos mas generalizados sobre los metodos formales son variaciones de los siguientes:
  1. Los metodos formales garantizan que el software esta perfecto. El mito mas importante es que los metodos formales serian todopoderosos, si nosotros humildes mortales pudiesemos aplicarlos. Este mito es pernicioso porque nos lleva a expectativas irreales y a la idea de que los metodos formales son de alguna forma todo o nada.
  2. Los metodos formales se centran en demostrar correccion. En los Estados Unidos, gran parte del trabajo desarrollado en metodos formales se ha concentrado en la verificacion de programas. Esto ha hecho que los metodos formales parezcan muy dificiles y no muy relevantes para la vida real.
  3. Los metodos formales son utiles solo para sistemas criticos. Esta creencia se basa en la percepcion de la dificultad que implica la aplicacion de metodos formales. La verdad es que los sistemas criticos requieren un uso mas acucioso de metodos formales, pero cualquier sistema puede beneficiarse con el uso de algunas tecnicas de especificacion formal.
  4. Los metodos formales requieren matematicos entrenados. Los metodos formales se basan en notaciones matematicas, y muchas personas creen que esto los hace dificiles para la practica de los ingenieros de software. Este mito, a su vez, se basa en la percepcion de que las matematicas son intrinsicamente dificiles.
  5. Los metodos formales aumentan el costo del desarrollo. Se acostumbraba decir que a pesar que el costo que significaba usar metodos formales era muy alto, de todas formas era conveniente porque resultaba en menores costos de mantenimiento del software.
  6. Los metodos formales son incomprensibles para los usuarios. Una especificacion formal esta llena de simbolos matematicos que resultan incomprensibles para cualquiera que no este familiarizado con la notacion. De ahi que se suponga que son inutiles para clientes no matematicos.
  7. Los metodos formales no se usan en grandes proyectos reales. Los metodos formales se asocian comunmente con departamentos academicos y organizaciones de investigacion. Se piensa que solo estas organizaciones tienen la capacidad necesaria para usar metodos formales y que estos solo son apropiados para las aplicaciones idealizadas que estos grupos desarrollan.
Principales Metodos Formales utilizados en el desarrollo de software
  • Metodos formales basados en Lógica de Primer Orden: Z, B, VDM, Object-Z, Z++ y VDM++.
  • Metodos formales basados en Formalismos Algebraicos: HOSA (Hidden Order Sorted Algebras), TROLL, OBLOG, Maude y AS-IS (Algebraic Specifications with Implicit States).
  • Metodos formales basados en Redes de Petri: CO-OPN (Concurrent Object-Oriented Petri Nets)
  • Metodos formales basados en Lógica Temporal: TRIO, OO-LTL y ATOM.
  • Metodos Semiformales: Syntropy, Statemate, UML y OCL (Object Constraint Language)

No hay comentarios:

Publicar un comentario