Ctividad 1. Análisis de casos de éxito de incorporación de métodos formales en el desarrollo del software.

[pic 1][pic 2]

Alumno: López Pérez Adriana Yolanda.

Matricula: 100909

Grupo: IS35

Materia: Métodos formales de ingeniería de software.

Asesor: Mtro. Emmanuel Hernández Ortiz.

Numero y tema de la actividad: Actividad 1. Análisis de casos de éxito de incorporación de métodos formales en el desarrollo del software.

Oaxaca de Juárez a 06 de  agosto de 2018.

Introducción

Por infraestructura crítica se entiende aquellas instalaciones, redes y tecnologías, cuya interrupción o destrucción puede tener una repercusión importante en la salud, la economía o el eficaz funcionamiento de los gobiernos. La criticidad de estos sistemas reside cada vez más en los softwares que contienen (Eterovic & Donadello, 2015) y la función que desempeñan. Las aplicaciones que brindan servicios vitales en estas infraestructuras se conocen como "software crítico” y son considerados de alta fiabilidad y seguridad (Matei, 2015). En estos sistemas se evidencia que las amenazas informáticas no sólo comprometen el mundo digital, sino que también son un riesgo mayor, para el mundo físico (Prieto, 2014). La seguridad del software se relaciona con la calidad, es una actividad del aseguramiento que se centra en la identificación y evaluación de los peligros potenciales que podrían afectarlo y ocasionar que falle (Pressman, 2010).

La clave de un software seguro es el proceso de desarrollo utilizado. En el proceso es donde se produce el producto que pueda resistir o sostenerse ante ataques no anticipados, recuperarse rápidamente y mitigar el daño causado por los ataques que no pueden ser eliminados o resistidos (Brito, 2013). Para la programación de software críticos de alta confiabilidad es imprescindible seguir una metodología en la que se defina cada paso, se utilicen una serie de herramientas de análisis, arquitecturas especiales, etc., para obtener diseños realmente confiables con unas características de coste y tiempo aceptables, y donde el esfuerzo se dirija tanto al hardware como al software (Pérez, 2006), sin dejar de lado el entorno en que se desarrolla.

The Encyclopedia of Software Engineering [Mar01] define los métodos formales en la forma siguiente:

Los métodos formales utilizados para desarrollar sistemas de cómputo son técnicas con base matemática para describir las propiedades del sistema. Tales métodos formales proporcionan marcos conceptuales dentro de los cuales las personas pueden especificar, desarrollar y verificar los sistemas en forma sistemática más que ad hoc.

1. Nombre del proyecto de software y una descripción.

IBM CICS transaction processing system: Este proyecto fue diseñado para ofrecer acceso a datos, comunicación, integridad y servicios de seguridad.

Entre las aplicaciones más conocidas del proyecto CICS se incluyen sistemas de compensación bancaria, control de almacenes, reservaciones aéreas y sistemas ATM, y cuenta con miles de licencias corporativas en el mundo.

Sistema CNS/ATM (comunicaciones, navegación, vigilancia y gestión del trafico aéreo).

En el mundo de la aviación se utiliza el termino CNS/ATM para referirse a los sistemas de comunicaciones aeronáuticas, navegación aérea y vigilancia y gestión del espacio aéreo. La gestión del espacio aéreo tiene como objetivo garantizar la seguridad de las aeronaves y conseguir que el operador de la aeronave pueda cumplir son su plan de vuelo.

1. Fase de diseño en donde se incorporó el método formal de software

Este método se uso durante la especificación de requisitos con esta notación Z se obtuvo una descripción precisa del sistema .

1. Información sobre el método formal obtenida de una fuente confiable

El lenguaje Z se basa en la teoría de conjuntos, calculo del lambda  y la lógica del primer orden.

Z es una notación formal, de Zermelo que utiliza los conceptos básicos de esta teoría (conjuntos, relaciones, funciones y variables) para describir sistemas. La notación proporciona una serie de tipos básicos, a los que se pueden añadir otros definidos por el diseñador.

Sobre estos tipos abstractos, Z define los llamados esquemas, que permiten la construcción estructurada y modular de aplicaciones de software. En Z los esquemas sirven para modelar tanto los aspectos estáticos (por ejemplo, los estados que puede alcanzar un sistema o los invariantes que deben conservarse en todos los estados) como los dinámicos (por ejemplo, las operaciones que pueden realizarse sobre el sistema, las relaciones entre las entradas y las salidas o la definición de cuando y como se producen los cambios de estado).

...