[VVS] 10. Propiedades de modelos de verificación

La tarea de esta semana consistió en lo siguiente:

• Inventen una expresión ω-regular con por lo menos dos símbolos y por lo menos dos operadores.
• Dibujen el NBA que le corresponde.

Un Autómata Büchi no determinista es una quintupla A = (Q, Σ, Q0, δ, F) sobre un abecedario Σ, donde:

• Q es un conjunto finito de estados
• Q0 ⊆ Q es un conjunto no vacío de estados iniciales
• δ : Q × Σ → 2^Q es una función de transición
• F ⊆ Q es un conjunto de estados finales.

Los operadores de un Autómata Büchi no determinista están definidos en la siguiente tabla

Operador	Símbolo	Representación
Unión	L1 ∪ L2 L1 + L2
Concatenación	L1 • L2 (L1)(L2)
Clausura	L1*

Para el ejemplo que tomaré, el abecedario estará dado por:

Σ = {a, b, c}

Y la expresión ω-regular será:

ab*+c

Podemos representar la expresión anterior construyendo el autómata paso a paso, primero la unión:

Despues dividimos la concatenación y resolvemos:

Por último la clausura, así obtenemos el autómata final.

Solo para complementar la información:

• Q = {q0, q1, q2, q3, q4, q5}
• Q0 = {q0}
• F = {q4}
• Σ = {a, b, c}

REFERENCIAS

• http://webdelprofesor.ula.ve/ingenieria/hyelitza/materias/preteoria/apuntes/tema2.pdf
• http://web.ing.puc.cl/~marenas/iic3800/clases/automata-1-imp.pdf
• [Libro] Principles of Model Checking - Christer Baier & Joost-Pieter Katoen

[VVS] 9. Modelado de Sistemas Concurrentes

La tarea consistió en elegir un sistema y modelarlo de 2 posibles maneras, ya sea mediante un sistema de transiciones o mediante un grafo de programa, elegí el sistema de transiciones.

El sistema que elegí fue una minimización de un restaurante de comida rápida.

Componentes:

• Cajero: Es el encargado de tomar las ordenes y pasarlas a la cocina para posteriormente cobrar el monto total del pedido.
• Cocina: Recibe las ordenes del cajero y se encarga de preparar el pedido, posteriormente sirve los platos para su posterior entrega.
• Ayudante: Se encarga de recibir los pedidos preparados por la cocina y los entrega al cliente, cerrando así el ciclo.

Siguiendo la nomenclatura del libro, el sistema completo queda definido por los componentes:

Modelado y descripción formal de los componentes:

Componente	Descripción	Modelado
Cajero	Estados {0} Espera {1} Orden recibida {2} Orden cobrada Acciones {Rec} Recibir la orden {Cob} Cobrar la orden {Pas} Pasar la orden a cocina
Cocina	Estados {0} Espera {1} Orden recibida {2} Orden preparada Acciones {Pas} Pasar orden (recibirla del cajero) {Pre} Preparar la orden {Ser} Servir la orden
Ayudante	Estados {0} Espera {1} Orden entregada Acciones {Ser} Servir la orden (Recibida de la cocina) {Ent} Entregar la orden al cliente

Diagrama de Transiciones

El sistema que elegí es altamente concurrente, es común que en un restaurante veamos a todo el equipo trabajando al mismo tiempo, por ejemplo, el cajero puede estar recibiendo ordenes constantemente y enviarlas a la cocina, no espera a que la cocina termine las ordenes, así mismo el ayudante quien constantemente entrega ordenes mientras el cajero y la cocina trabajan.

Es por ello que encontré múltiples caminos a diversos estados, pero se puede notar un miniloop con los estados {000} → {100} → {200} → {010} → {020} → {001} que indican el camino de la transición si el sistema no fuera concurrente

Referencias:

• [Libro] Principles of Model Checking - Christer Baier & Joost-Pieter Katoen

[VVS] 8. Verificación formal de sistemas

Una Red de Petri es un modelo gráfico, formal y abstracto para describir y analizar el flujo de información, sirven como una herramienta matemática para modelar concurrencia, no deterninismo, comunicación y sincronización.

El análisis de las Redes de Petri ayuda a mostrar información importante sobre la estructura y el comportamiento dinámico de los sistemas modelados.

http://astreo.ii.uam.es/~jlara/doctorado.2006/tema7.pdf

Las redes de petri fueron inventadas por el alemán Karl Adam Petri en 1962. En su tesis doctoral "kommunikation mit automaten" (Comunicación con autómatas) establece los fundamentos para el desarrollo teórico de los conceptos básicos de las redes de petri.

Las redes petri son consideradas una herramienta para el estudio de los sistemas, con una red de petri se puede modelar el comportamiento y la estructura de un sistema. Posteriormente se puede analizar el flujo del proceso que el sistema realiza para obtener un resultado, asi como obtener información sobre el comportamiento dinámico del sistema.

Las redes de petri se componen de dos cosas:

• Lugares: que permiten representar los estados del sistema mediante la utilización de marcas.
• Transiciones: que representan el conjunto de acciones a realizar cuando se cumplen unas determinadas precondiciones en el sistema.

Más ampliamente, una red de Petri es un conjunto formado por la tupla R = {P, T, Pre, Post}, la tupla contiene los componentes básicos que forman su estructura:

• Un conjunto de plazas P
• Un conjunto de transiciones T
• La función de entrada I
• La función de salida O

Las funciones de entrada y salida relacionan las transiciones y las plazas.

La función de entrada I es un mapeo a partir del conjunto de plazas de entrada hacia la transición tj, la función se puede escribir como I(tj).

La función de salida O es un mapeo a partir de la transición tj hacia el conjunto de plazas de salida, la función de salida se puede escribir como O(tj).

Ejemplo de Red de Petri: http://www.uhu.es/diego.lopez/AI/auto_trans-tema3.PDF

Hay una serie de condiciones que deben cumplirse en la construcción de las Redes de Petri:

1. Un arco une siempre lugares con transiciones y nunca dos lugares o dos transiciones.
2. Una transición puede ser destino de varios lugares y un lugar puede ser el destino devarias transiciones.
3. Una transición puede ser origen de varios lugares y un lugar puede ser origen de varias transiciones.
4. Los lugares pueden presentar marcas (una marca se representa mediante un punto en el interior del círculo).
5. Cada lugar tiene asociada una acción o salida. Los lugares que contiene marcas se consideran lugares activos. Cuando un lugar está activo sus salidas están a uno.
6. A las transiciones se les asocia eventos (funciones lógicas de las variables de entrada). Una transición se dice que está sensibilizada cuando todos su lugares origen están marcados.
7. Cuando ocurre un evento asociado a una transición (la función lógica se hace uno), se dice que la transición está validada.

Algunas de las aplicaciones de las Redes de Petri pueden ser diseñar, analizar y diagnosticar:

• Sistemas concurrentes
• Arquitetura de Computadores
• Protocolos de Redes
• Sistemas Operativos
• Sistemas de Producción
• Sistemas Digitales
• Hardware/Software
• Sistemas de Tiempo Real
• Control de Tráfico

Mas información, consultar referencias.

Actividad

La actividad de esta semana consistió en:

• Investigar un poco sobre Redes Petri
• Inventar un pequeño sistema concurrente
• Modelar la Red Petri en Python, utilizando python-snakes

El sistema concurrente que elegí se me ocurrio viendo una maquina de café en el trabajo, asi que comencé a diseñar una red de petri de acuerdo a cómo pienso que funciona esa máquina.

Primero, ¿qué hace la máquina? Básicamente tiene 2 botones, agua o café, y dependiendo de cuál botón presiones dispensará agua caliente o una infusión de café.

Para ello note el siguiente flujo de trabajo:

• La máquina está en espera
• Presionas el boton de agua caliente o café.
• Si eliges café, la maquina toma un poco de café, lo muele y lo coloca en el filtro
• La máquina comienza a hacer fluir el agua caliente por el filtro
• La máquina dispensa la infusión de café.
• La máquina limpia el filtro y espera nuevamente.
• Si eliges agua caliente la máquina se brinca los pasos de tomar, moler y colocar el café, solamente hace fluir el agua caliente y vuelve a esperar.

Ahora, hay 2 transiciones que suceden en silencio.

• Verificar si hay café en el contenedor, si no, enciende un led rojo como aviso.
• Verificar si hay agua en el contenedor, si no, enciende un led rojo (diferente) como aviso.

Entonces, identifiqué los siguientes estados y transiciones:

Estados	Transiciones
Esperando Agua seleccionada Café seleccionado Si hay café Si hay agua Bebida servida No hay café No hay agua	Selecciona bebida Verificar café Verificar agua Servir bebida Limpiar filtro Aviso error

El dibujo queda algo asi:

Utilizando python-snakes:

Diagrama animado:

Código:

Referencias
http://pommereau.blogspot.mx/search/label/SNAKES
http://pommereau.blogspot.mx/2010/01/first-steps-with-snakes.html
http://pommereau.blogspot.mx/2010/01/firing-rule-in-snakes.html
http://pommereau.blogspot.mx/2010/01/snakes.html
http://code.google.com/p/python-snakes/source/browse/doc/tutorial.txt?spec=svn.abcd.b7e58afd5c1b845899816065fff49d782e02a56b&repo=abcd&r=b7e58afd5c1b845899816065fff49d782e02a56b
http://www.uhu.es/diego.lopez/AI/auto_trans-tema3.PDF

[VVS] 7. Aplicaciones de la lógica predicativa

Esta tarea consistio en investigar una aplicación práctica de la lógica de primer orden, el tema que elegí fue la aplicacion de la lógica de primer orden para la verificación de protocolos de seguridad

Definición

Un protocolo es un conjunto de reglas que establecen cómo se debe realizar la transmisión de datos de cualquier tipo entre 2 entidades. Sin un protocolo común, los dos dispositivos pueden estar conectados pero no comunicarse.

Un protocolo debe tener 3 caracteristicas:

• Sintaxis (¿Cómo se comunica?) Orden en que se agrupan los datos para formar el mensaje.
• Semántica (¿Qué se comunica?) Significado de cada parte del mensaje.
• Temporización (¿Cuándo se comunica?) Cuándo se debe enviar el mensaje.

En los protocolos de seguridad existen además 2 elementos importantes, cada uno con sis propieas caracteristicas:

• Mensaje:
• Confidencialidad
• Integridad
• Autenticación
• No repudio
• Entidades que se comunican:
• Realizan autenticación

Un protocolo de seguridad se compone habitualmente de dos partes:

• Criptográfica: que es el cifrado de los datos
• Lógica: que define la estructura y el orden de los mensajes.

Protocolos de seguridad y lógica de primer orden

La mayoría de las debilidades en un protocolo se encuentran en la parte lógica debido a que no es posible analizar todas las aplicaciónes que éste pueda tener, entonces las pruebas se limitan a suposiciones de cómo el protocolo será utilizado y bajo qué condiciones.

La lógica de primer orden permite realizar un análisis previo a la liberación del protocolo.

Para verificar un protocolo, hay que probar dos cosas:

• Que el protocolo consigue sus objetivos (postcondiciones) cuando se ejecuta cada uno de los pasos especificados en el diseño (casos de uso del protocolo).
• Que no hay posibilidad de un ataque (es decir, no se puede usar el protocolo de forma fraudulenta).

Analicemos el caso del protocolo RSA, la parte criptográfica consiste en los siguientes pasos:

• Se eligen dos primos muy grandes p y q.
• Se calcula n = (p) (q), el cual será el módulo para cifrado y descifrado.
• Se calcula φn = (p − 1) (q − 1).
• Se elige un número aleatorio e y se calcula d, de forma que d = e^-1 mod φn.
• La pareja de numeros (e, n) forman la clave pública.
• La pareja de números (d, n) forman la clave privada.

Los mensajes se cifran con (e, n) y sólo se puede descifrar con (d, n) y viceversa.

La seguridad del protocolo RSA depende del tamaño de n, ya que, dada la clave pública es posible obtener la clave privada factorizando n.

La parte lógica del protócolo, por ejemplo, trata las siguientes cuestiones:

• ¿Cómo saber si el usuario que dice ser Bob es realmente Bob?
• ¿Es suficiente utilizar una contraseña?
• ¿La contraseña debe ser cifrada con la clave pública del servidor? 
• Analizar confidencialidad, integridad, autenticación, no repudio.

La exactitud del protocolo (que éste sea correcto) se analiza definiendo axiomas y reglas de inferencia comunes de la logica de primer orden y adicionalmente se agregan axiomas que represetan las caracteristicas y propiedades de seguridad que debe tener el protocolo. Mediante esta sintaxis es posible demostrar algunas de las propiedades de seguridad del protocolo directamente.

Estas pruebas logicas garantizan que las propiedades sean verdaderas y comprueba que el protocolo es robusto.

Protocolo simétrico de Needham-Schroeder

En éste protocolo cada mensaje se puede interpretar como una acción que modifica el estado de creencia de los individuos que intervienen en la comunicación

Se necesitan enviar 3 mensajes para establecer una comunicación segura, cuando se han enviado los tres mensajes cada uno de los agentes sabe que el otro es quien dice ser.

Las condiciones iniciales del protocolo son las siguientes:

• S es un servidor confiado por ambas partes
• K_AS es una clave simétrica que conocen sólo A y S
• K_BS es una clave simétrica que conocen sólo B y S 
• NA y NB son nonces (número, puede ser pseudoaleatorio, de un solo uso que se usa como un sencillo método adicional de autenticación).

Las propiedades del protocolo, utilizando la lógica de primer orden, se escriben de la siguiente forma:

• A → S : A,B,NA
• S → A : {NA, K_AB, B, {K_AB, A}_KBS}_KAS
• ==============================================
• A → B : {K_AB, A}_KBS
• B → A : {N_B}_KAB
• A → B : {N_B-1}_KAB

El protocolo se lee de la siguiente forma:

• Alice se comunica con el servidor, se identifica a si misma y a Bob y envía un nonce. (Solicta comunicarse con Bob)
• Servidor responde a Alice, genera la clave K_AB y la envía a Alice junto con el nonce y la autenticación de Bob, además envía un paquete con la clave K_AB y la autenticación de Alice, cifrado con la clave K_BS (que solo Bob y el servidor conocen). La totalidad de la información esta cifrada con la clave que solo Alice y el servidor conocen.

Los tres mensajes de autenticación consisten en lo siguiente:

• Alice decifra la información, recupera el nonce (garantiza que la información corresponde a su sesión y que es reciente), la clave K_AB y la autenticación de Bob. Como hay un paquete cifrado con K_BS el paquete se envía a Bob para que también tenga su copia de la clave K_AB. y de la autenticación de Alice.
• Bob responde a Alice con un nonce cifrado con K_AB (clave que solo conocen Alice y Bob), con ello demuestra que recibio la clave.
• Alice responde a Bob con un nonce modificado (mediante una operación simple) cifrado con la clave , con ello demuestra que tiene la clave también.

Asi queda comprobado que Alice y Bob son quien dicen ser.

Protocolo de clave pública de Needham-Schroeder

Las condiciones iniciales para éste protocolo son:

• K_PA y K_SA claves pública y privada de Alice.
• K_PB y K_SB claves pública y privada de Bob.
• K_PS y K_SS claves pública y privada del servidor.

Utilizando lógica de primer orden, el protocolo se representa de la siguiente forma:

• A → S : A, B
• S → A : {K_PB, B}_KSS
• A → B : {NA, A}_KPB
• B → S : B, A
• S → B : {K_PA, A}_KSS
• B → A : {NA, NB}_KPA
• A → B : {NB}_KPB

El protocolo se lee:

• Alice solicita al servidor la clave pública de Bob
• El servidor responde con la cláve pública de Bob y con si identidad, la información esta cifrada con la clave secreta del servidor.
• Alice conoce la clave pública del servidor, decripta la información y envía un nonce a Bob con su identidad, todo cifrado con la clave publica de Bob.
• B solicita al servidor la cláve pública de Alice.
• El servidor responde con la cláve pública de Alice y con si identidad, la información esta cifrada con la clave secreta del servidor.
• Bob genera otro nonce y lo envía a Alice junto con el nonce que recibio de Alice, la información va encriptada con la clave pública de Alice.
• Alice reponde a Bob con el nonce recibido NB, encriptado con la clave pública de Bob.

Al finalizar el protocolo, Alice y Bob estan seguros de ser quien decían ser.

Lógica de BAN

Es un método formal que permite difinir y analizar las propiedades de los protocolos. Fue

desarrollado con los aportes de Michael Burrows, Martin Abadi y Roger Needham.

Es una extensión de la lógica de primer orden que se basa en creencias de los agentes que participan en el protocolo.

Objetivo

Lógica de BAN intenta responder las siguientes preguntas:

• ¿Cuál es el objetivo del protocolo a analizar?
• ¿El protocolo necesita mas suposiciones que algún otro?
• ¿El protocolo realiza una acción innecesaria que puede eliminarse sin debilitarlo?
• ¿El protocolo encripta información que puede ser enviada en texto plano sin debilitarlo?

Limitaciones

La principal limitación es que siempre asume una criptografia perfecta:

• Los agentes nunca publican la información secreta, pero no se encarga de verificar que se cumpla.
• Los agentes reconocen los fallos, pero no verifica la ausencia de los mismos.
• Los agentes reconocen o ignoran mensajes enviados por ellos mismos.
• Los agentes son honestos.
• Agentes comprometidos no estan considerados
• Los atacantes no tienen claves válidas.

Sintaxis

• Identificadores para los agentes. (A, B, C, ...)
• Identificadores para las llaves. (k)
• Identificadores para funciones atomicas. (n)
• Conjunto de formulas. (X , Y, Z, ...)

Las formulas pueden ser expresadas por ejemplo: "A cree que k es una llave compartida entre A y B", y dan siempre como resultado verdad o falso.

Formulas

Tomada de http://wwwhome.cs.utwente.nl/~sape/sse/ban.pdf

1. P cree X: P tiene razones para creer que el mensaje X es verdad.
2. P ve X: P puede ver el mensaje X y puede reproducirlo.
3. P dijo X: En algún momento P envió el mensaje X.
4. Fresco(X): El mensaje X pertenece al presente (sesión actual) y no ha sido utilizado antes.
5. P controla X: P tiene pertenencia sobre X. (Tiene, controla, o conoce)
6. P y Q comparten la llave K, K es buena para establecer comunicación entre ambos.
7. P tiene la clave pública K
8. X es un secreto solo y solo entre P y Q
9. X combinada con la función Y.
10. {X}_K : X encriptada con la llave K

Algunos ejemplos donde se aplican las anteriores formulas son las siguientes formulas:

	P cree que la llave K esta compartida con Q. P vee que X esta encriptado con la llave pública K. Entonces P cree que Q dijo X.
	P cree que Q tiene la llave publica K. P vee que X esta encriptado con la llave privada K-1. Entonces P cree que Q dijo X.
	P cree que Y es un secreto entre él y Q. P vee que X se utiliza en la fórmula Y. Entonces P cree que Q dijo X
	P cree que X fue mencionado recientemente. Q alguna vez dijo X. Entonces P cree que Q cree en X.
	P cree que a Q le pertenece X. P cree que Q cree en X. Entonces P cree en X.

Fuente: A Logic of Authentication

Protocolo Needham-Schroeder y Lógica de BAN

Como ejemplo, vamos a analizar el protocolo Needham-Schroeder (especificado más arriba) utilizando la lógica de BAN.

Recordando las condiciones iniciales:

K_A y K_A^-1 claves pública y privada de Alice.

K_B y K_B^-1 claves pública y privada de Bob.

K_S y K_S^-1 claves pública y privada del servidor.

Las propiedades del protocolo quedarían de la siguiente forma:

A cree que tiene la llave pública KA	B cree que tiene la llave pública KB
A cree que S tiene la llave pública KS	B cree que S tiene la llave pública KS
S cree que A tiene la llave pública KA	S cree que B tiene la llave pública KB
S cree que tiene la llave pública KS
A cree que S conoce la llave de B	B cree que S conoce la llave de A
A cree que su nonce NA es reciente (fresco)	B cree que su nonce NB es reciente (fresco)
A cree que su nonce NA es un secreto entre él y B	B cree que su nonce NB es un secreto entre él y A
A cree que el mensaje con la llave pública de B, KB es reciente	B cree que el mensaje con la llave pública de A, KA es reciente

En resumen, cada uno A y B tienen un par de llaves las cuales con conocidas por S. Los nonces son creados para esa sesión especifica y cada uno conoce su nonce. Ambos utilizan sus llaves públicas durante la sesión de comunicación.

Ahora, la debilidad del protocolo se encuentra justamente en las 2 ultimas creencias, a pesar de que son llaves públicas, A y B no conocen las llaves del otro hasta que cada uno la envía al otro, esto provoca que dicho mensaje no sea fresco, sino que pudo haber sido envíado por un tercero quien lo encripto previamente. Para solucionar este problema de agregan 4 creencias más:

A cree que B tiene la llave pública KB	B cree que A tiene la llave pública KA
A cree que B cree que el nonce NA es un secreto entre ellos	B cree que A cree que el nonce NB es un secreto entre ellos

Ahora, ambos confirman su llave pública mutuamente y además intercambian su nonce para asegurar que es fresco en ambos casos, ahora ambos creen que el otro dice la verdad por lo que pueden continuar el intercambio de información.



Referencias

• Wikipedia: Protocolo de Needham-Schroeder
• University of Cambridge Computer Laboratory: A Logic of Authentication
• BAN Logic: A Logic of Authentication by Sape J. Mullender
• Verification of Security Protocols Chapter 6: BAN Logic by Christian Haack
• Métodos formales para la verificación de protocolos: http://grupo.us.es/ghum609/php/system/files/fernando1.pdf
• Protocolos de seguridad: http://ldc.usb.ve/~poc/Seguridad/protocolos.pdf

[VVS] 6. Principios de demostraciones de validez

Para la tarea de esta semana se eligió un ejercicio del texto http://www.logicinaction.org/docs/ch4.pdf, el ejercicio que elegí fue el siguiente:

Exercise 4.5: Rephrase "¬( X ≤ Y ∧ Y ≤ Z )" in predicate logic, using binary relations "<" for "less than" and "=" for "equal"

Ejercicio 4.5: Reformular "¬( X ≤ Y ∧ Y ≤ Z )" en lógica predicativa, usando las relaciones binarias "<" para "menor que" y "=" para "igual"

Solución

Expresión incial: 

¬( X ≤ Y ∧ Y ≤ Z )

La expresión nos dice que "no es verdad que Y es mayor o igual a X y no es verdad que Y es menor o igual a Z", en pocas palabras "Y no esta en el rango desde X hasta Z".

Debemos eliminar los símbolos de "mayor o igual que" para cumplir con lo que el ejercicio nos pide, entonces primero podemos ir reduciendo la expresión paso por paso para entender lo que vamos haciendo.

Primero, la teoría nos dice que expresiónes con las siguiente estructura:

A < B ∧ A < C   ó   A > B ∧ A > C

pueden ser reformuladas removiendo el conectivo and y quedando de la siguiente manera:

A < B < C   ó   A > B > C

Entonces nuestra expresión puede reformularse así:

¬( X ≤ Y ≤ Z )

Segundo, podemos eliminar los símbolos de "mayor o igual que" tal como nos lo recomienda el mismo ejercicio, utilizando dos relaciones binarias y uniéndolas con un conectivo lógico, así, la expresión:

A ≤ B 

puede reformularse así:

A < B ∨ A = B

y nuestra expresión queda así:

¬[ ( X < Y < Z ) ∨  ( X = Y = Z ) ]

FIN :)

[VVS] 5. Lógica predicativa de primer y segundo orden

Para ésta tarea fue necesario elegir un ejercicio del libro Lean Symbolic Logic de Lewis Carroll.

El ejercicio elegido es el número 11 y se encuentra en la página 101, y dice:

"Audible music causes vibrations in the air.

Inaudible music is not worth paying for."

"La música audible causa vibraciones en el aire.

No vale la pena pagar por música inaudible"

El primer paso para hallar la conclusión es definir algunas equivalencias en notación simbólica-lógica, definí las siguientes:

• A(x) : Música audible.
• ¬A(x) : Música no audible (inaudible).
• C(x) :  Causa vibraciones.
• ¬C(x) : No causa vibraciones.
• P(x): Vale la pena pagar.
• ¬P(x) : No vale la pena pagar.

El segundo paso es combinar los cuantificadores con las notaciones anteriores:

• ∀ : Para todos
• ∃ : Por lo menos uno, alguno

Ahora sustituímos para obtener las siguientes sentencias

• Audible music causes vibrations in the air.          ∀(x)A(x) ⇒ C(x)


• Inaudible music is not worth paying for.              ∀(x)¬A(x) ⇒ ¬P(x)

El último paso es analizar las sentencias anteriores y obtener algunas conclusiones y otras sentencias lógicamente equivalentes, pude identificar las siguientes:

• Is worth paying for music if causes vibrations in the air.                   P(x) ⇒ C(x)


• No music is worth paying for unless it causes vibrations in the air.  ¬P(x) ∨ C(x)

Referencias

• "Lean Symbolic Logic" by  Lewis Carroll
• http://www.scribd.com/doc/7365560/Introduction-to-Logic-06-Propositional-Logic

[VVS] 4. Diagramas binarios de decisión

"Este tipo de diagramas sirven para representar simbólicamente los estados del sistema y las funciones booleanas de forma compacta"

Instrucciones

La tarea 4 consiste en realizar lo siguiente:

• Inventar una función booleana, usando por mínimo 3 variables y 4 conectivos básicos.
• Construyan y dibujen su BDD.
• Reduzcan el BDD resultante a un ROBDD.
• Dibujen el ROBDD resultante.

Expresion

[ ( A ∧ B ) ∧ ¬C ] ∨ ¬B

Tabla de Verdad

A	B	C	(A ∧ B)	¬C	((A ∧ B) ∧ ¬C)	¬B	(((A ∧ B) ∧ ¬C ) ∨ ¬B
0	0	0	0	1	0	1	1
0	0	1	0	0	0	1	1
0	1	0	0	1	0	0	0
0	1	1	0	0	0	0	0
1	0	0	0	1	0	1	1
1	0	1	0	0	0	1	1
1	1	0	1	1	1	0	1
1	1	1	1	0	0	0	0

Árbol de Decisión

Con la expresión anterior formamos el siguiente diagrama:

Después procedemos con la reducción, eligiendo aquellas hojas que terminan en el mismo valor y fusionandolas en una sola, y tomando también aquellas ramas con la misma estructura y fusionandolas en una sola:

[1]

 [2]

Y ésta es la máxima reducción que logramos con el orden actual de las variables.

[3]

Referencias:

• http://www.cs.us.es/cursos/lp-2005/temas/tema-07.pdf
• http://www.cs.unb.ca/~gdueck/courses/cs4835/bdd97.pdf

[VVS] 3. Aplicaciones de la lógica proposicional

[1] "La Lógica Proposicional pretende estudiar las frases declarativas simples (enunciados o proposiciones) que son los elementos básicos de transmisión de conocimiento humano. 

De manera informal, una proposición se define como una frase que puede ser considerada verdadera o falsa y que no se puede descomponer en otras frases verdaderas o falsas."

[2] "Una de las razones que motivó la aparición de la lógica matemática, fue evitar la ambigüedad del lenguaje natural y transformar el pensamiento en un cálculo, según el modo de operar de las matemáticas. Simplificar o simbolizar las oraciones o juicios para poder operar con ellas, así surge el lenguaje formal."

Algunos conceptos

La lógica proposicional representa el lenguaje de una forma bastante simplificada y primitiva que nos analizar muchas deducciones sobre el mundo que nos rodea.

El objetivo principal la lógica proposicional es el razonamiento, utilizando un mecanismo que primero evalúa sentencias simples y luego sentencias complejas, formadas mediante el uso de conectivos proposicionales, por ejemplo Y (AND), O (OR). Este mecanismo determina la veracidad de una sentencia compleja, analizando los valores de veracidad asignados a las sentencias simples que la conforman.

Una proposición es una simple oración que tiene un valor asociado de verdad (V), o falso (F), pero nunca puede tener ambos, algunos ejemplos pueden ser:

• El día esta soleado
• Mañana es jueves
• Los hombres son mortales
• Jose es hermano de María

Los conectivos proposicionales utilizados juntar las oraciones son:

Nombre	Símbolo	Lenguaje Natural	Ejemplo
Conjunción	∧	... y ...	Esta nublado y esta lloviendo
Disyunción	∨	... o ...	Esta nublado o esta soleado
Negación	¬	no ...	No esta nublado
Implicación	→	si... entonces ...	Si esta nublado entonces esta lloviendo
Doble Implicación	↔	... sí y solo sí ...	Esta lloviendo si y solo si esta nublado

La sintaxis de la lógica proposicional contiene un alfabeto que esta formado por:

• Las constantes lógicas de verdad y falso (V, F)
• Los símbolos de las variables (letras del alfabeto)
• Los conectivos proposicionales (las tablas de arriba)
• Símbolos de puntuación como paréntesis, corchetes y llaves

La unión de los componentes anteriores forman una oración compuesta.

La semántica le da un significado a las expresiones del lenguaje lógico y permite interpretar cada uno de los elementos del alfabeto logico y darle a su vez un valor de verdad o falso a cada una de las proposiciones, el valor esta definido por las tablas de verdad:

Negación
P	¬P
V	F
F	V

Conjunción
P	Q	P∧Q
V	V	V
V	F	F
F	V	F
F	F	F

Disyunción
P	Q	P∨Q
V	V	V
V	F	V
F	V	V
F	F	F

Implicación
P	Q	P→Q
V	V	V
V	F	F
F	V	V
F	F	V

Doble Implicación
P	Q	P↔Q
V	V	V
V	F	F
F	V	F
F	F	V

Al terminar analizar una oración proposicional podemos toparnos con 4 posibles casos:

• Tautología o validez: Cuando todas las combinaciones de una proposición dan como conclusión verdad
• Contradicción: Cuando todas las combinaciones de una proposición dan como conclusión falso
• Contingencia: Cuando no tenemos suficiente información para obtener una conclusión y la proposición puede ser verdad o falso
• Satisfabilidad: Si una combinación de todas las posibles es verdadera

Sistemas basados en conocimientos

Con los anteriores conceptos aterrizados, llegamos a otros 2 conceptos que ya son las bases de los sistemas basados en conocimientos:

• Inferir: Es tomar una decisión a partir de algo que ya conocemos, y asi llegar a una conclusión.
• Razonar: Es pensar con coherencia y lógica para establecer inferencias.

Existen 3 tipos de razonamiento:

• Deducción: Razonar algo de lo conocido a lo desconocido, comenzando con algo general a algo específico. Siempre se usan inferencias correctas lo que concluye en una conclusión verdadera.
• Abducción: Razonamiento que comienza con una conclusión e intenta hacer a la conlusión válida. No siempre garantiza que la conclusión sea verdadera.
• Inducción: Razonamiento que comienza con casos individuales para obtener una conclusión general. El conocimiento esta basado en éste método y permite el aprendizaje.

Asi pues "[3] un sistema basado en conocimiento (ABC) es aquel sistema que posee conocimiento de su mundo y es capaz de razonar sobre las posibles acciones que puede tomar para cambiar el estado de su mundo"

Razonamiento y conocimiento son importantes para estos sistemas pues son la base de su comportamiento exitoso.

Éstos sistemas constan de 3 partes importantes:

• Base de conocimiento que es un conjunto de oraciones que representan hechos del mundo real. Cada hecho es una oración. Por lo general hechos para los que fue programado el sistema de un tema específico. 
  Estos sistemas realizan 2 tareas importantes:
  • Decir para agregar conocimiento
  • Preguntar para obtener conocimiento y qué acción realizar ante una situación. (Cada pregunta se responde mediante el razonamiento lógico.)
• Motor de Inferencia que es el que deduce nuevas oraciones a partir de la base de conocimiento y de las nuevas oraciones almacenadas despues del proceso de aprendizaje. Aqui se utilizan teorías, que son las reglas que se deben seguir para inferir oraciones desde otras oraciones.
• Base de hechos que es una pseudo-memoria a largo plazo donde se almacenan las conclusiones correctas.

Tomada de http://www.monografias.com/trabajos12/inteartf/inteartf2.shtml

Estos sistemas también tienen percepción que es la manera en la que entran los datos

La importancia de la lógica proposicional en el tema no es mínima, digamos que la lógica proposicional juega un papel importante en el lenguaje de representación de conocimiento, que junto con la lógica del predicado y lógica temporal forman lo que se conoce como lógica formal.
El lenguaje de representación de conocimiento se utiliza para representar los hechos que el sistema procesará y unn ejemplo lenguaje de representación de conocimiento es PROLOG

Los sitemas basados en conocimientos que pueden en un futuro convertirse en sistemas para toma de decisiones o sistemas con inteligencia artificial.

[4] "Una lógica es un sistema formal para describir lo que esta sucediendo en un momento determinado y que consta de:

• Sintaxis: Reglas que explican cómo construir oraciones o sentencias legales.
• Semántica: Cómo las oraciones representan hechos en el mundo.

Si la semántica y la sintaxis están definidas de manera precisa, se dice que el lenguaje es una lógica."

Los componentes de un lenguaje de representación de conocimiento son:

• Predicados: Son los atributos de los elementos.
• Elementos: Son las proposiciones.
• Constantes: Son una identidad completa, como un objeto o individuo.
• Variables Lógicas: Son binarias (V,F) y son aquellas que vamos evaluar.
• Variable anónima: Es una variable sin nombre y referenciada
• Operadores: Son los mismos que los operadores proposicionales.
• Hechos: Son relaciones entre los predicados y elementos
• Reglas: Son las condiciones entre los hechos y por lo general son implicaciones.

Referencias

• [1] http://www.cs.buap.mx/~iolmos/propeLogica/1_LP1.pdf
• [2] http://www.educared.org/wikiEducared/L%C3%B3gica_proposicional.html#Lenguaje_formal
• [3] http://www.slideshare.net/leopoldocapa/agentes-lgicos-presentation
• [4] http://www.monografias.com/trabajos51/inteligencia-artificial/inteligencia-artificial.shtml
• http://www.slideshare.net/leopoldocapa/agentes-lgicos-presentation
• http://www.monografias.com/trabajos/iartificial/pagina4_1.htm
• http://www.fismat.iteso.mx/pag_def/estructura/matematicas/asignaturas/logicamatematica2004/apoyos/proposicional3.pdf
• www.nebrija.es/~cmalagon/ia/transparencias/representacion_del_conocimiento_prolog.pdf

[VVS] 2. Lógica proposicional; formas normales

Después de un pequeño recordatorio sobre matemáticas discretas y lógica proposicional, la tarea 2 consistío en armar una tautología.

Aterrizando el concepto:

"Una tautología es aquella fórmula lógica que es cierta para cualquier valoración de los símbolos proposicionales que contiene."

Sin embargo, la tautología a elaborar debía tener las siguientes caracteristicas:

• 3 variables
• 4 conectivos lógicos
• Por lo menos 1 disyunción, 1 conjunción y 1 negación

La tarea fue sencilla, no llevo mucho tiempo, los pasos que segui fueron:

1. Armar una tabla de verdad para las 3 variables
2. Agregar el primer conectivo, una conjunción y resolver
3. Agregar el segundo conectivo, una disyunción y resolver
4. Agregar el tercer conectivo, una implicación y resolver para la conjunción y la disyunción, elegí la implicación por el resultado de los anteriores conectivos, se ve que se puede obtener una tautología antes.
5. Aplicar un cuarto conectivo, la negación a la tercer variable.
6. Agregar el quinto conectivo, una disyunción, elegí este conectivo para obtener con seguridad una tautología al final ya que es el único que me da el resultado que busco.

Ésta es la tabla de verdad con todo el procedimiento:

p	q	r	(p ∧ q)	(p ∨ q)	((p ∧ q) -> (p ∨ q))	¬r	(((p ∧ q) -> (p ∨ q)) ∨ ¬r)
V	V	V	V	V	V	F	V
V	V	F	V	V	V	V	V
V	F	V	F	V	V	F	V
V	F	F	F	V	V	V	V
F	V	V	F	V	V	F	V
F	V	F	F	F	V	V	V
F	F	V	F	V	V	F	V
F	F	F	F	F	V	V	V

Éste es el árbol correspondiente a la tautología que arme:

Segundo Intento

Edito la entrada, pues no debí haber usado la implicación, entonces, partiendo del mismo procedimiento modifico del paso 4 en adelante:

1. Tabla con 3 variables
2. 1 conjunción
3. 1 disyunción
4. Negar la conjunción
5. Unir la conjunción negada y la disyunción con otra disyunción adicional

Ésta es la tabla de verdad con todo el procedimiento:

p	q	r	(p ∧ q)	(p ∨ q)	(¬(p ∧ q))	((¬(p ∧ q)) ∨ (p ∨ q))
V	V	V	V	V	F	V
V	V	F	V	V	F	V
V	F	V	F	V	V	V
V	F	F	F	V	V	V
F	V	V	F	V	V	V
F	V	F	F	F	V	V
F	F	V	F	V	V	V
F	F	F	F	F	V	V

Éste es el árbol correspondiente a la nueva tautología:

[VVS] 1. La Verificación y Validación de Software

DEFINICIÓN

Conjunto de procesos de comprobación y análisis que aseguran que el software que se desarrolla está acorde a su especificación y cumple las necesidades de los clientes.

OBJETIVO

Los objetivos de las actividades de verificación y validación son valorar y mejorar la calidad de los productos del trabajo generados durante el desarrollo y modificación del software. Debemos corregir todo posible fallo y alcanzar cierto grado de perfección, asi mismo, debemos garantizar la consistencia, confiabilidad, utilidad, eficacia y el apego a los estándares del desarrollo de software.

Para ello es necesario encontrar defectos en el sistema que estamos desarrollando y asegurarnos que el sistema será útil para el entorno de trabajo requerido.

VERIFICACIÓN Y VALIDACIÓN

Ambos conceptos suelen tratarse como sinónimos, sin embargo, se refieren a cosas completamente distintas:

• La verificación se enfoca más al proceso de evaluación del sistema o de los componentes, permite determinar si los productos de una determinada fase del desarrollo satisfacen las condiciones impuestas en el inicio de la misma. Responde la pregunta ¿Estamos construyendo el producto correctamente?, entonces el software debería ajustarse a sus especificaciones iniciales.
• La validación también es una evaluación del sistema o componentes, pero solo se efectúa en el transcurso o al final del proceso del desarrollo para determinar si cumple con lo especificado. Responde la pregunta ¿Estamos construyendo el producto correcto?, entonces el software debería hacer lo que el cliente realmente quiere que haga.

Es importante resaltar que nunca se va a poder demostrar que el software está completamente libre de defectos, la verificación y validación mas crítica es realizada por los clientes finales.

TÉCNICAS DE VALIDACIÓN Y VERIFICACIÓN

Para aplicar estas técnicas siempre en necesario modelar cierto tipo de pruebas (tests) específicas, las pruebas son actividades en las cuales un sistema o uno de sus componentes se ejecuta en circunstancias previamente especificadas, los resultados se observan y registran y se realiza una evaluación de algún aspecto.

Varias pruebas juntas con un fin especifico constituyen un caso de pruebas donde un conjunto de entradas, condiciones de ejecución y resultados esperados son desarrollados para un objetivo particular.

Las pruebas deben centrarse en dos objetivos:

• Probar si el software no hace lo que debe hacer.
• Probar si el software hace lo que no debe hacer, es decir, si provoca efectos secundarios.

Se clasifican en 2 grandes grupos:

• Inspecciones de Software: analizan y comprueban las representaciones del sistema (los diagramas de diseño, el código fuente del programa). Se aplica a todas las etapas del proceso de desarrollo y se complementan con algún tipo de análisis automático del texto fuente y documentos asociados. Son técnicas de verificación y validación estáticas, no requieren que el sistema se ejecute.
• Pruebas de Software: consisten en comparar datos teóricos con los resultados del software utilizando series de datos de prueba, se examinan los resultados del software y su comportamiento operacional para comprobar que se desempeñe conforme a lo requerido. Es una técnica dinámica de la verificación y validación ya que requiere disponer de un prototipo ejecutable del sistema.

Lo que buscamos descubrir con ambos tipos de pruebas son:

• Defectos (bug): un defecto en el software como, por ejemplo, un proceso, una definición de datos o un paso de procesamiento incorrectos en un programa.
• Fallos (failure): La incapacidad de un sistema o de alguno de sus componentes para realizar las funciones requeridas dentro de los requisitos de rendimiento especificados.

Los errores mas comunes son:

• División por cero
• Ciclo infinito
• Problemas aritméticos como desbordamientos (overflow) o subdesbordamientos (underflow).
• Exceder el tamaño del array
• Utilizar una variable no inicializada
• Acceder a memoria no permitida (access violation)
• Pérdida de memoria (memory leak)
• Desbordamiento o subdesbordamiento de la pila (estructura de datos)
• Desbordamiento de búfer (buffer overflow)
• Bloqueo mutuo (deadlock)
• Indizado inadecuado de tablas en bases de datos.

Después de que hemos realizado ambas pruebas y que han sido localizados errores, es necesario especificar un proceso de depuración .

El proceso de depuración localiza y corrige los errores descubiertos durante la verificación y validación. Es un proceso complicado pues no siempre los errores se detectan cerca del punto en que se generaron. Para este paso„ se utilizan herramientas de depuración, que facilitan el proceso. Algunos ejemplos de herramientas de depuración para diferentes plataformas son:

• GDB (GNU Project Debugger) para C jdb - The Java Debugger
• JDB (Java Debugger) para JAVA
• JUnit (Java Unit Testing), suite de pruebas unitarias para JAVA , existen versiones para JavaScript.
• PDB (Python debugger), suite de pruebas unitarias para JAVA

Después de reparar el error, hay que volver a probar el sistema (pruebas de regresión)pues la solución del primer fallo puede dar lugar a nuevos fallos.

IMPORTANCIA

La importancia de los procesos de validación se puede entender mejor si analizamos las consecuencias de no realizarlos, hay varios ejemplos famosos: : El Cohete Mariner 1, en una investigación espacial destinada a Venus, se desvió de su trayectoria de vuelo poco después de su lanzamiento. El control de la misión destruyó el cohete pasados 293 segundos desde el despegue. Causa: Un programador codificó incorrectamente en el software una fórmula manuscrita, saltándose un simple guión sobre una expresión. Sin la función de suavizado indicada por este símbolo, el software interpretó como serias las variaciones normales de velocidad y causó correcciones erróneas en el rumbo que hicieron que el cohete saliera de su trayectoria.

• Desastre: Cohete Mariner 1 
  Descripción: investigación espacial destinada a Venus, se desvió de su trayectoria de vuelo poco después de su lanzamiento. El control de la misión destruyó el cohete pasados 293 segundos desde el despegue. 
  Causa: Un programador codificó incorrectamente en el software una fórmula manuscrita, saltándose un simple guión sobre una expresión. Sin la función de suavizado indicada por este símbolo, el software interpretó como serias las variaciones normales de velocidad y causó correcciones erróneas en el rumbo que hicieron que el cohete saliera de su trayectoria.


• Desastre: Mars Climate Orbiter 
  Descripción: El satélite se estrello en la superficie marciana. 
  Causa: error en la programación del sistema de navegación hizo que al entrar en su atmósfera este se desintegrara, esto pasó porque al introducir los cálculos no se hicieron en el Sistema Métrico Internacional lo que provocó un fallo en la medición de la altitud sobre el planeta.


• Desastre: Ariane 5 
  Descripción: El cohete se desvía se su curso debido a un error en los datos procesados. El intento posterior de enderezar la trayectoria fue demasiado brusco y el cohete finalmente se destruyó a los 37 sg. 
  Causa: el software de control realizó una conversión de un valor flotante de 64 bits en un entero de 16 bits sin comprobar que se produjeran desbordamientos.

Todos los desastres anteriores pudieron haber sido evitados si la causa de los mismos hubiera sido corregida mediante sencillas pruebas y evaluaciones.

Como podemos suponer, este tipo de experimentos tienen un alto costo para las instituciones que los realizan, un error en el sistema puede resultar en la perdida de millones de dolares, aunque en la actualidad son mas serios los errores que tienden a corromper o suprimir la información o datos guardados de los usuarios.

Siempre hay que darle importancia a estas pruebas y destinar los recursos necesarios a las mismas, no solo por las perdidas y el costo de repararlos en una etapa posterior, sino por nuestra propia ética profesional, un error de este tipo puede dejar a un Ingeniero en Software sin trabajo de por vida, entonces, es necesario ver las técnicas de validación y verificación de software como un proceso obligado en el desarrollo de software.

REFERENCIAS

• http://www.oscargallardo.com/wp-content/uploads/2011/04/CIISA_IS2_V_V2.ppt
• http://clases3gingsof.wetpaint.com/page/Verificación+y+Validación
• http://www.ctr.unican.es/asignaturas/Ingenieria_Software_4_F/Doc/M7_09_VerificacionValidacion-2011.pdf