martes, 20 de noviembre de 2012

Tarea. 12

Para esta tarea seleccione el porblema 2.6 el cual dice lo siuiente:

Whenever p is true, it cannot be true again until both q and r have been true (q and r need not have been true simultaneously)

-cuando p es verdadero, no puede ser verdad otra vez hasta que ambos q y r haber sido cierto (q y r no necesita ser verdad al mismo tiempo)

El problema nos pide si el enunciado se puede traducir en un CTL

Yo opino que si se puede:



martes, 13 de noviembre de 2012

Tarea

Seleccione el siguiente ejercicio del Linear Temporal Logic LTL el cual menciona:


A holds at all states s3k and does not hold at all states s3k+1 , s3k+2 , where k = 0, 1, . . ..



Basandonos en lo siguiente relizaremos el problema:



=holds at all states s3k 

 not hold at all states s3k+1 , s3k+2+




En conclusion A solo tiene los estados 0s3,1s3,2s3,3s3... pero no tiene los estados s3+1,2s3+2



lunes, 15 de octubre de 2012


Tarea 7: Aplicación de la Lógica Predictiva

Hola compañeros y Dra. en esta entrada les hablare de una aplicación de la lógica predictiva  llamada Sistema axiomático.

Sistema axiomático


Este método consiste en aceptar sin prueba ciertas proposiciones como son los axiomas o algunos postulados y después de esos axiomas en derivar todas las proposiciones del sistema, en calidad ya de teoremas. Los axiomas son los cimientos del sistema y los teoremas las superestructuras.

Enfoque axiomático 

El enfoque axiomático puede interpretarse como una máquina que produce formas predicativas, de acuerdo con: reglas sintácticas, reglas de validez y axiomas.
Características de un enfoque axiomático:
  • El concepto de verdad aparece como accesorio
  • Su modelo se conforma por tres partes:
    • Un cálculo
    • Reglas de transformación
    • Axiomas
    •   
Modelo del enfoque axiómatico

Cálculo: Nos dice  cómo es que se construirán formas proposicionales correctas, o fórmulas bien formadas (fbf), del lenguaje.

Alfabeto (signos primitivos):
  • coma: {,}
  • paréntesis: {( , )}
  • Conectivos primitivos: {∨,
  • ¬}
  • Cuantificador universal: {∀}
  • Constantes individuales: Ac = {a, b, c,..., a1, b1, c1,...}
  • Variables individuales: Av = {x, y, z,..., x1, y1, z1,...}
  • Símbolos de predicado: Ap = {P, Q, R,...,P1, Q1, R1 ...}
  • Símbolos de función: Af = {f, g, h,..., f1, g1, h1,...}
Reglas de formación de fórmulas:
  • Cualquier fórmula atómica es una fbf.
  • Si R y S son fbfs, entonces R ∨ S es una fbf.
  • Si R es una fbf, entonces (R) es una fbf.
  • Si R es una fbf, entonces ¬R es una fbf.
  • Si R es una fbf, entonces ∀x R es una fbf.

Definición de otros signos complementarios
  • Pueden emplearse otros conectivos lógicos como: ∧, →, y ↔ para crear fbfs. Su
  • definición corresponde a las vistas en el cálculo proposicional.
  • También puede introducirse el signo de cuantificador existencial ∃, definido como
  • sigue:  ∃x P ↔ ¬∀x ¬P, donde P es una fbf.
Axiomas

Son fbfs iniciales que se emplean para generar fbfs dentro del sistema axiomático.
  • Axioma de Idempotencia
  • Axioma de Adjunción
  • Axioma de Conmutatividad
  • Axioma de Adición
  • Sean P y Q fbfs, entonces la fbf ∀x(P → Q) → (P → ∀xQ) es un axioma, siempre que P no posea  ocurrencias libres de x.
Reglas de inferencia
  • Modus Ponems
  • Sustitución
  • Ejemplificación Universal (E.U.)
    • Sea la fbf ∀xP, entonces se puede obtener la fbf Px|t.
    • Donde P es una fbf y el término t es libre de la variable x en P.
Casos:
  • De la fbf ∀xP se puede producir la fbf Px|x .
  • De la fbf ∀xP se puede obtener la fbf P, donde x es una variable sin ocurrencias libres en P.
  • De la fbf ∀xP se puede obtener la fbf Px|a, donde a es una constante individual.

  • Ejemplificación Existencial (E.E.)
  • Sea la fbf ∃x P, entonces se puede producir la fbf Px|t.
  • Donde P es una fbf y el término t es libre de la variable x en P.
Restricciones:

La variable x no puede exhibir ocurrencias libres en alguna de las premisas o en alguna fbf obtenida en un paso previo de la deducción.
No aparecer el término t en la fbf de la conclusión, en alguna premisa o una fbf
obtenida en un paso previo de la deducción.

Casos:

De la fbf ∃xP se puede obtener la fbf Px|x
De la fbf ∃xP se puede producir la fbf P, donde x es una variable sin ocurrencias libres en P.
De la fbf ∃xP se puede producir la fbf Px|a, donde a es una constante individual.

Observación:
Si el término t es un símbolo de variable, éste se torna fijo al representar un individuo
que no se conoce pero se sabe que existe y, por tanto, no puede efectuarse ninguna
generalización universal sobre él posteriormente.



  • Generalización Universal (G.U.)
    • Si P es una fbf, entonces se puede obtener la fbf ∀xP


Restricciones:

x no posee ocurrencias libres en alguna premisa.
No se permiten generalizaciones universales a partir de P si en ésta el símbolo x se obtuvo de la aplicación previa de la E.E.


  • Generalización Existencial (G.E.)
    • Sea P una fbf, entonces se puede producir la fbf ∃xP.

Donde P es una fbf y la variable x debe originarse de un
término que en P aparezca como una constate individual o una
variable libre.

Leyes importantes:

∀xP ↔ P donde x no posee ocurrencias libres en la fbf P.
∃xP ↔ P donde x no posee ocurrencias libres en la fbf P.
∀xP ↔ ∀yPx|y donde y no posee ocurrencias libres en la fbf P.
∃xP ↔ ∃yPx|y donde y no posee ocurrencias libres en la fbf P.

Intercambio de cuantificadores

∀x P ↔ ¬ ∃x ¬ P
∃x P ↔ ¬ ∀x ¬ P
¬ ∀x P ↔ ∃x ¬ P
¬ ∃x P ↔ ∀x ¬ P

Negación de expresiones con varios cuantificadores

¬ ∀x ∀y P ↔ ∃x ∃y ¬ P
¬ ∃x ∃y P ↔ ∀x ∀y ¬ P
¬ ∀x ∃y P ↔ ∃x ∀y ¬ P
¬ ∃x ∀y P ↔ ∀x ∃y ¬ P

Propiedades conmutativas

∀x ∀y P ↔ ∀y ∀x P donde P es una fbf
∃x ∃y P ↔ ∃y ∃x P donde P es una fbf
∃x ∀y P → ∀y ∃x P donde P es una fbf

Leyes distributivas

∀x(P ∨ Q) ↔ ∀xP ∨ Q donde P y Q son fbfs, Q no posee ocurrencia  libres de x.
∃x(P ∧ Q) ↔ ∃xP ∧ Q ∀xP ∨ ∀xQ → ∀x(P ∨ Q) donde P y Q son fbfs, Q no posee ocurrencia libres de x.  donde P y Q son fbfs
∀x(P ∧ Q) ↔ ∀xP ∧ ∀xQ donde P y Q son fbfs
∃x(P ∧ Q) → ∃xP ∧ ∃xQ donde P y Q son fbfs
∃x(P ∨ Q) ↔ ∃xP ∨ ∃xQ donde P y Q son fbfs
∀x(P → Q) → (∀xP → ∀xQ) donde P y Q son fbfs
∀xP ∨ ∀yQ ↔ ∀x ∀y (P ∨ Q) donde P y Q son fbfs; además y no posee ocurrencias libres en P y x no posee ocurrencias libres en Q.


Otras

∀x(P →Q) ↔ (∃xP → Q) donde Q no posee ocurrencias libres de x.
∃x(P → Q) ↔ (∀xP → ∃xQ)
(∃xP → ∀xQ) → ∀x(P → Q)
(∃xP → ∀xQ) → (∀xP → ∀xQ)
∀x ∀y ∀z(P ∧ Q → R) ↔ ∀x ∀z (∃y (P ∧ Q) → R); donde la fbf P tiene ocurrencias libres de x y y, la fbf Q posee ocurrencias libres de y y z, y la fbf R posee ocurrencias libres de x y z.


Observaciones a tener en cuenta en procesos demostrativos:

Es diferente P | Q de | P → Q. En el primero, P es una premisa; en el segundo, P debe tratarse como una hipótesis auxiliar.
Cuando se encuentre en un proceso demostrativo, aplique primero la ejemplificación existencial que la universal.
Si P es una fbf, es posible sustituir cualquier subexpresión, o fbf, B de A, por una fbf C, siempre y cuando B y C hallan sido demostradas como equivalentes. (Esta es una forma de expresar la R.V. sustitución).
Cuando en un proceso de prueba sólo se emplee la R.V. sustitución, el resultado obtenido es lógicamente equivalente a la expresión de la cual surgió. Esto implica que en algunos procesos demostrativos de bicondicionales, requieran sólo demostrarse un solo sentido.
Demostrar una fbf A, es equivalente a demostrar que la fbf ¬A lo lleva a una contradicción.
No poder demostrar una fbf A, es equivalente a no poder probar que la fórmula ¬A lo lleva a una contradicción.



Bibliografía:

lunes, 17 de septiembre de 2012

Problema 4.24 Lógica de predicados se pueden utilizar para contar dos gráficas separadas: encontrar una fórmula que es cierto en el uno, pero no en la otra. Considere las siguientes dos imágenes:




Dar una fórmula, y R para la relación, cierto en el lado izquierdo y falso a la derecha

Como vemos la imagen anterior se compone de flechas dirigidas lo que lo hace un grafo dirigido, estas flechas dirigidas son llamadas bordes.




En el libro viene una explicación la cual es la siguiente:



Nos dice que la imagen es un grafo dirigido y que las siguientes formulas son correctas para que lo representemos:

$\mathbf{ \exists x\exists yRxy}$

$\mathbf{\exists xRxx}$

$\mathbf{\rightharpoondown \forall x\exists yRxy}$

Como en este caso que el primer grafo la relación es reflexiba y seria $\mathbf{xRy}$ por eso es verdadera si existe por lo menos una x y una y.

Propiedad Transitiva



La cual se representa de la siguiente manera:

$\mathbf{xRy \wedge  yRz\rightarrow xRz}$





Figura 1



Nos piden la relacion y en este caso la relaciòn es transitiva, ya que siempre hay flechas de x a y y de y a z.


Figura 2



Como vemos aquí no hay ninguna relación transitiva, por lo cual vamos a formular la relación con la transitiva para que el grafo 1 sea verdadero y el 2 sea falso.

¿Por que no usamos la simétrica ni la reflexiva?, no la usamos ya que los dos grafos tienen relación simétrica y reflexiva y no podríamos tener una formula que sea falsa para la segunda.

Formula:

$\mathbf{\exists x\exists y\exists z\left ( Rxy \wedge  Ryz \right )}$

$\mathbf{\exists x\exists y\exists z\left ( Rxy \wedge  Ryz \right )}$ es verdadera si existe por lo menos una x,y y z que 

Entonces llegamos a la conclusión que es verdadera para la izquierda y falsa para la derecha ya que la derecha no tiene relación transitiva 




viernes, 7 de septiembre de 2012

Tarea 5: Lógica Predictiva 

En la tarea 5 seleccionamos un ejercicio del libro  Lean Symbolic Logic de Lewis Carroll, en este caso me toco el ejercicio numero 38:


No emperors are dentists 
All dentists are dreaded by children 
No emperors are dreaded by children. 

Traducción español:

No hay emperadores que sean dentistas
Todos los dentistas son temidos por los niños
No hay emperadores que sean temidos por los niños

No hay=Ningunos

E(x): emperors(emperadores)
D(x): dentists(dentistas)
N(x): dreaded by children(temidos por los niños)

Simbolos fundamentales que usaremos:

$\forall$: cuantificador universal (todos)
$\exists$ : cuantificador existencial (existe)

Sustituimos las palabras por símbolos:


  • No emperors are dentists : $\mathbf{\rightharpoondown\exists (x) E(x)\to D(x)}$
  • All dentists are dreaded by children: $\forall (x)D(x)\to N\left ( x \right ) $
  • No emperors are dreaded by children: $\mathbf{\rightharpoondown\exists (x) E(x)\to N(x)}$


Conclusión:

Some people, dreaded by children, are not emperors

Someone dreaded by children, are not emperors: $\mathbf{\exists (x) N(x)\to \rightharpoondown E(x)}$




Referencias:

Link1
Link2
Link3
Link4

domingo, 2 de septiembre de 2012

Tarea 4:


 1-. Inventen una expresión Booleana.                   
           Usando por mínimo 3 variables y 4 conectivos básicos.
2-. Construyan y dibujen su BDD.
3-. Reduzcan el BDD resultante a un ROBDD.

4-. Dibujen el ROBDD resultante.


1-. Inventen una expresión Booleana.  

(((p^r)^(p|q))|^((¬r)|(p^q)))^¬q


Como vemos nuestra expresión Booleana tiene tres variables y cuenta con los 4 conectivos que son:
¬ : Negación
| = conjunción
^ = disyunción
 = Implicación


Después realizamos la tabla de verdad de la expresión:




Después realice el árbol binario de desición:

En el arbol la linea gris es 1 y la linea gris punteada es 0.




2-. Construyan y dibujen su BDD(Binary Decisión Diagram).

Para poder construir un Diagrama Binario de Desición se toma en cuenta:

1. Quitar los nodos terminales repetidos: Dejamos un solo nodo 0 y 1
2. Quitar los nodos no terminales repetidos (coinciden la variable y los hijos)
3. Quitar tests redundantes (coinciden los dos hijos)












3 y 4 -. Reduzcan el BDD resultante a un ROBDD y dibujarlo:

Cambie la posición de las variables como se muestra a r,q,p.

Como vemos se redujo a 4 nodos de los 5 que teniamos.

Referencias: DBB


jueves, 30 de agosto de 2012

Tarea2:

 La tarea 2 es checar si las claves que genera nuestro otp (one time pad) realmente es aleatoria.

 La clave evaluada fue la siguiente:


Esta clave es generada del programa anterior con el siguiente código:

Funciona leyendo las claves del archivo llamado key.txt pasandoselo a cada uno de los test.



Primero yo realice un test sencillo que se llama Monobit:

Monobit

Detecta los ceros y los unos que se encuentran en la cadena binaria, sustituyendo los ceros que encuentre por -1, asi realizando una suma. La aparición de ceros y unos en la secuencia global deberan de ser igualmente probables

Datos a tener:

n = tamaño de la clave binaria
ε =La secuencia de bits que se esta probando

Procedimiento:

1. Como mencione se buscan los ceros y se sustituyen por -1y se realiza una suma, ejemplo:
   lista=[1,1,0,0,1,0,1]
   quedaría:
   lista=[11,-1-1,1-11]
 y se realiza la suma de la lista

2-Se calcula la prueba estadística:





3. Se calcula p_value ( erfc es la función error complementaria.)


4.Si P - value > 0.01, la secuencia  es aleatoria.

Código:

Captura de pantalla de la prueba:



También utilice otras dos pruebas que es la de Poker y la de frecuencia de Bloques

Frecuencia de Bloques

En la prueba de bloques los ceros y unos deberan de ser igualmente probables.
 Datos:

n - largo de la secuencia
m - el largo de cada bloque
ε - secuencia de bits generada

Recomendaciones:










Procedimiento:

1. Se parte la prueba e bloques de un cierto tamaño se calcula de la siguiente manera:
  

2. Se determina la proporción de unos:


3. Se calcula la chi2=X2


4.  Se calcula la p_value:






Código

Captura de pantalla



Prueba de Póker

Lo que hace la prueba de póker es dividir la clave en numeros de 4 bist, por ejemplo si yo tengo esta:

0101000001100011

se divide de la siguiente manera :
0101 0000 0110 0011

entonces como se divide en 4 hay 16 posibles resulados que pueden salir y esos 16 resultados son contados las veces que estan o el número de frecuencias de cada uno.

La formula que se realiza es la siuiente:

en donde:
m = es el tamaño de la división de la secuencia en este caso 4
n = lóngitud o tamaño de la secuencia binaria
k = es la división de m entre n

Pasos:

1. Se divide la serie de número binarios en secciones de 4 numeros (0000).
2. Se buscan las frecuencias de los 16 diferentes numeros que se pueden encontrar
3. La frecuencia se eleva al cuadrado
4. Se realiza lo que es la ecuación anterior:

         x2=(16/k)(frecuencias al cuadrado)-k

La prueba se pasa cuando 1.03 < x < 57.4

Captura de pantalla


Con otra cantidad de claves:

Monobit



Frecuencia de Bloques



Poker test




La clave pasa las pruebas eso quiere decir que es segura.

Referencias:

Link1
Link2
LInk3

lunes, 27 de agosto de 2012

Aplicaciones de la lógica Proposicional


Entre las aplicaciones que podemos encontrar de la lógica proposicional se encuentran las relacionadas con:



  • Inteligencia Artificial:Representación de conocimiento, razonamiento con sentido común.
  • Bases de Datos: Lenguajes de consulta, lenguajes para restricciones de integridad.
  • Ingeniería de Software: Espeiento con sentido común:
  • Teoría de la Computación: complejidad descriptiva, algoritmos de aproximación.
  • Criptografía: verificación de protocolos criptográficos.
  • Procesamiento de Lenguaje Natural

Comenzaremos por definir algunas de las aplicaciones relacionadas con lo anterior descrito y otras que no se mencionaron:

-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. 
Inteligencia Artificial 
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.


Representación de conocimiento:

La ingeniería cognoscitiva ha adaptado diversos sistemas de representación del conocimiento que se aproximan a los elaborados por la psicología cognoscitiva para el cerebro humano. Aquí es donde juega parte de esto la lógica proposicional.

-La lógica proposicional se aplica en el lenguaje al momento de realizar la representación del conocimiento.

Razonamiento con sentido común:

Lo que nos hace diferente de otros seres humanos es que nosotros razonamos acerca de lo que sucede diariamente. El sentido común es la creencia que tenemos nosotros como peronas, en relación a lo que consideramos mas prudente o razonable sobre algún tema,, auqnue no tengamos algún sustento.

El Razonamiento de Sentido Común en la IA tiene como objetivo establecer soluciones para simulación de formas de razonamiento que realizamos nosotros de forma natural en la solución de problemas en escenarios dle mundo real y que han resultado dificiles de abordar con técnicas que se basan en enfoques matemáticos.

La resolución para cláusulas de Horn que resulta de la evolución de los sitemas de Base de Datos y los lenguajes de programación lógica como Prolog y sus extensiones a la programación lógica y con restricciones y la programación lógico-funcional.

-.-.-.-.-.-.-.-.-.-.-.-.
Base de Datos:
-.-.-.-.-.-.-.-.-.-.-.-.



Los lenguaje de consulta como su nombre lo indica son lenguajes con los cuales el usuario puede consultar información de una base de datos.

Las consultas se representan como fórmulas de lógica proposicional.




La operación select se define:



donde p es una fórmula en cálculo proposicional que consta de términos conectados por: ∧ (and), ∨ (or), ¬ (not) y cada término sigue la expresión:

<attribute> op {<attribute> | <constant>}

donde op es: =, ≠, >, ≥, <, ≤



-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
Lenguajes de Programación
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.




Como ya la mayoría de nosotros sabemos que Prolog es un lenguaje de Programación lógico e interpretado.

La lógica proposicional tiene una gran aplicación en lo que es el lenguaje Prolog.




Sintaxis de la lógica proposicional en Prolog:



Declaración de operadores:

:-op(610,fy,-). % negación
:-op(620,xfy,&). % conjunción
:-op(630,xfy,v). % disyunción
:-op(640,xfy,=>).%condicional
:-op(650,xfy,<=>).% equivalencia

-Las técnicas de reescritura , la aplicación de reglas lógicas que son la base de la programación funcional como por ejemplo LISP, ML, de diversas aplicaciones en inteligencia artificial como son los sistemas expertos y la bases de conocimiento, de ciertos sistemas de álgebra por ordenador.

-.-.-.-.-.-.-.-.-.
Criptografía
-.-.-.-.-.-.-.-.-.






En la criptografía se utiliza para la verificación de protocolos criptográficos los cuales se usan cuando se requiere privacidad, autentificación como por ejemplo la firma electronica.



Aparte de lo anterior mencionado también se aplica para la síntesis y verificación de circuitos y sistemas entre los que se encuentran los reactivos, asíncronos, ocurrentes y distribuidos, al igual que nos sirve para resolver problemas de la vida real como horarios, rutas de transporte y la planificación
de obras.


Referencias:

Link1
Link2
Link3
Link4
Link5
Link6
Link7
img1
img2
img3|
img4

martes, 21 de agosto de 2012

Tautología

Una tautología es una formula de un sistema de lógica proposicional que resulta verdadera para cualquier interpretación.


 En clase se pidio realizar una tomando las si(((q | p)| (p ^ r))| ((¬q)|(¬ p)))entes restricciones:

  •  Minimo utilizar 3 variables  
  • Utilizar los operadores lógicos and, or y not
  • Minimo tener 4 operadores (por ejemplo utilizar los tres anteriores y uno repetido)
YO realize un programita que trabajaba con tres variables en este caso "p", "q" y "r", el cual nos creaba grupos de 4 o 3 o del tamaño q quisieras.

Salidas del programa

Proposición 1




Esta un poco revuelto, para una mejor comprensión vamos a ir checando de uno por uno:

not = ¬
or = |
and = ^

La salida es: (r or q)and (r and p)or (not r)and (not p)

seria: (r|q)^(r ^p)| (¬ r)^(¬ p)

Y se preguntan ¿Qué se hace primero? yo aqui utilize la prioridad de los operadores lógicosque primero seria la negación, después la conjunción(and) y al final la disyunción(or).

Quedaria asi: (((r|q)^(r ^p))| ((¬ r)^(¬ p)))

La tabla de verdad quedaria de la siguiente manera:


La tabla tiene las mismas salidas que nos da el programa, to solo imprimi el resultado.


Proposición 2:


La salida es: (r or p)and (q and r)or (not p)and (p or r)

seria: (r | p)^(q^r)| (¬p)^(p|r)

Quedaria asi: (((r | p)^(q^r))| ((¬p)^(p|r)))

La tabla de verdad quedaria de la siguiente manera:


Las salidas son las mismas que la que nos devuelve el programa

A la tercera proposición el programa nos arrojo una tautología:

Proposición 3


La salida es: (q or p)or (p and r)or (not q)or (not p)

seria: (q | p)| (p ^ r)| (¬q)|(¬ p)

Como al unir los grupos son puras uniones con or no importa cual se haga primero ya que dara el mismo resultado.

Quedaria asi: (((q | p)| (p ^ r))| ((¬q)|(¬ p)))

La tabla de verdad quedaria de la siguiente manera:




Como ya obtuvimos la tautología lo que aremos sera realizar el árbol correspondiente:


Código


Algunas cosillas que se le podian aplicar al código seria que el programa terminara hasta que encontrara una tautologia.

Algunas otras tautologías:




 
Prioridad de los operadores lógicos:


martes, 14 de agosto de 2012

Tarea 1

El objetivo de la verificación y validación son para poder mejorar la calidad de los productos del trabajo    que son generados durante el dessarrollo y modificación del software

La verificación esta más enfocada a lo que es el proceso de evaluar el sistema que determina si los productos de una fase determinada:

  • Construir el sistema correctamente.
  • Descubrir y corregir errores en el Sistema desarrollado.
  • Tipos: estática y dinámica
  • Criterios a verificar:
  • Consistencia: vigilar que la información sea coherente
  • Precisión: corrección de la sintaxis. Errores morfológicos.
  • Completitud: lagunas en capacidad deductiva.
  • Identifica desviaciones con estándares y requerimientos.
  • Recolecta datos para mejorar el proceso (es opcional).
  • Verifica que el producto cumpla:



Mientras que la validación también es una evaluacion del sistema  o componentes que determina la fase del desarrollo que satisfacen las condiciones que se recalcaron al inicio de la etapa.

  • Construir el sistema correcto.
  • Actividad ‘viva’ no sobre el papel.
  • Según ANSI/IEEE ‘evaluar la conformidad con la especificación de requisitos’


Verificación Formal

La Verificación Formal consiste en un conjunto de técnicas de comprobación formales que permiten demostrar si un programa funciona correctamente.

A continuación voy a describir algunos hechos en donde se da a conocer que una Verificación Formal es necesaria y asi nos ahorrariamos muchos problemas como grandes perdidas de dinero y muchos accidentes.


1965-Sonda Espacial Mariner I
 


Se menciona que no fallo por que sus calculos no eran correctos o que tuviera algun error en un componente sino por que la formula encargada de la trayectoria del cohete para ponerse en orbita no se transcribio correctamente  a lenguaje informático.

Se menciona que a los 4 min y 53 s hubo una inclinación hacia el noreste en el cohete que no era esperada, ya que debido a esta inclinación surgio la posibilidad de que este callera en el Océano Atlántico cerca de las rutas transatlánticas, y se envio un comando al cohete para su autodestrucción 6 s antes de que soltase la sonda.





1993-Error de cálculo en los Intel Pentium

En 1993 Intel tenia un error en que causo muchas perdidas de dinero, el error se encontraba en algo tan simple que en si era un error de calculo, la cantidad de chips diseñados fue entre 3 y 5 millones de chips    con un error del 0.006 % a la hora de dividir un número de punto flotante.  Con tal error estos chips nos son inservibles cuando se realiza aplicaciones de alta precisión. La perdida fue de 475 millones de dólalres, esto no solo afecto a los usuarios sino también a la imagen de la compañía.

Eurofighter

El Eurofighter Typhoon un avión militar ya que en la realización de estos primeros aviones al intentar probarlos uno de los tests consistía en simular un fallo de uno de los dos motores del avión, apagándolo para ver cómo reaccionaba el avión con un solo motor. El motor se apago  los pilotos se dieron cuenta de que el otro motor también tenía la misma respuesta y ya que se llego a la altura minima las personas que realizaban tuvieron más remedio que eyectarse. Después de tiempo investigando acerca del fallo del error se dieron cuenta que este se encontraba con que el software estaba mal programado, esto se debia al cierre erróneo de la válvula de combustible, que no odía ser abierta nuevamente en el vuelo. 


 Generador de claves Kerberos


 El generador de claves Kerberos se convirtio en un sistema de seguridad informática, el error fue que la semilla aleatoria que se utilizaba no era tan aleatoria. Hasta el momento no se conoce el alcance del fallo ya que por ejemplo si una compañía estuviera protegida con esto no lo diria, mas que nada por imagen.











Referencia: