Lógica Temporal

Verificación y Validación de Software
Entrada 11

Para esta semana seleccionamos un ejercicio del PDF mencionado al final de esta publicación, referente a lógica lineal temporal (LTL, por sus siglas en inglés).

El ejercicio seleccionado fue el 14.1.6 y la traducción literal del enunciado es el siguiente.

Si un estudiante olvida una moneda en la ranura de monedas, otro estudiante usará esta moneda para obtener una bebida antes de que cualquier profesor pueda hacerlo.

Entonces usando los operadores temporales tenemos:

$\square (eom \Rightarrow \circ(¬pum \ R \ eum))$

Donde:
eom = Estudiante Olvida Moneda
pum = Profesor Usa Moneda
eum = Estudiante Usa Moneda

Recursos consultados:
Linear Temporal Logic

Autómata Büchi No-Determinista

Verificación y Validación de Software
Entrada 10

Para esta semana se nos pidió hacer lo siguiente:

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

Abecedario

$\sum {\left\{A, B, C\right\}}$

Expresión ω-regular

$(A^*B)(AC+C)^w$

Autómata Büchi No-Determinista

La siguiente imagen es un paso intermedio antes de llegar al autómata completo, aquí solo están las transiciones entre tres estados, donde tales transiciones son la separación por el AND de la expresión.

Y el autómata completo es el siguiente.

Entonces tenemos $L = \{Q, \sum, \delta, I, F\}$

Donde:
$Q = \{q0, q1, q2, q3\}$
$\sum = {\left\{A, B, C\right\}}$
$\delta$ son las transiciones mostradas en la imagen
$I = \{q0\}$
$F = \{q3\}$

Referencias:
Course On Principles Of Model Checking
Automata On Infinite Words

Grafo de Programa

Verificación y Validación de Software
Entrada 9

Para esta semana se nos pidió que modeláramos un sistema simple y lo representáramos mediante un sistema de transiciones o un grafo de programa, y opcionalmente crear la representación en PROMELA.

El sistema que modele para esta semana es muy simple. Se trata de la máquina donde se paga el pasaje en el Transmetro.

Descripción:
En el transporte "Transmetro" cuando un pasajero aborda el camión debe de ingresar la cantidad de $4.50 en la máquina. Una vez ingresada tal cantidad, se imprime un boleto con un código de barras. Esto se hace para evitar hacer doble pago al llegar a la estación, ya que con el mismo boleto del camión es posible subir al Metro.

Tomando en cuenta la máquina que recibe el dinero e imprime lo boletos, modele el sistema, que como podemos ver es muy simple, ya que solo consiste en una máquina que espera el ingreso de monedas, este esta contando el total, y cuando se tiene ya 4.50 en la máquina, se imprime un boleto. También hay que tomar en cuenta que no regresa cambio.

Por ser algo simple de entender, me pareció más práctico dibujar el sistema directo a un grafo de programa.

De la forma en que yo lo modele, supongo que desde que la máquina es encendida inicializa una variable para contar y otra que dice de cuanto fue la moneda. Hay un bucle al que entra inmediatamente después de esto, donde se espera a ingresar una moneda y se suma a la cantidad actual, y no se sale de ahí hasta que el total sean 4.50. Después de salir se imprime el boleto y se resta 4.50 al total, para regresar de nuevo al estado donde se espera el ingreso de monedas.

Es posible que el trabajo de esta máquina no sea secuencial sino que sea algo de forma paralelizada, por un lado la parte que toma las monedas, y por otro la que imprime el boleto. Esto se puede ver cuando un grupo de personas sube al camión, y solo una persona se encarga de depositar el dinero de todos en la máquina. La máquina no necesita que el usuario deje de meter monedas para poder imprimir los boletos, sino que cada que sobrepasa la cantidad de $4.50 imprime un boleto y resta la misma cantidad del total.

Entonces podemos verlo como dos tareas independientes de la siguiente forma.

Contador de monedas
Impresión del boleto

Representación PROMELA

PROMELA (Process/Protocol Meta Language) es un lenguaje de modelado de verificación. El lenguaje permite la creación dinámica de procesos concurrentes de un modelo, por ejemplo, los sistemas distribuidos. En modelos PROMELA, la comunicación a través de canales de mensajes puede ser definido para ser sincrónico o asincrónico. Un modelo escrito en PROMELA se puede analizar con el comprobador de modelos SPIN, para verificar que el sistema modelado produce el comportamiento deseado. [1]

Instalar SPIN en Ubuntu

1. Descargar la versión más reciente y compatible con tu sistema del ejecutable Spin. En mi caso he descargado el archivo spin622_linux64 para Linux.

Spin Precompiled Executables

2. De forma opcional es posible descargar un complemento gráfico para ejecutar y depurar el código. Aquí descargue el archivo ispin.tcl, que solo requiere de tener instalado el paquete tk8.4.

Spin Sources

3. Si no tienes instalado el paquete tk8.4, o no estas seguro de si ya lo tienes ejecuta el siguiente comando, si no esta instalado te pedirá tu aprobación para iniciar la instalación, en caso contrario te dirá que no es necesario instalar ningún paquete extra.

~$ sudo apt-get install tk8.4

4. Ahora vamos a la carpeta donde guardamos los archivos descargados y copiamos el ejecutable a la carpeta /usr/bin/ con el nombre de spin.

~$ cd Downloads/promela/
~$ sudo cp spin622_linux64 /usr/bin/spin

5. Para abrir la interfaz gráfica, estando en la carpeta donde tenemos guardado nuestro archivo ejecutamos la siguiente instrucción.

~$ wish ispin.tcl

6. Si quieres correr tus programas desde terminal solo es necesario ejecutar la siguiente instrucción, donde hello.pml es el nombre del archivo donde tienes tu código.

~$ spin -n2 hello.pml

Regresando al grafo de programa que mostré anteriormente, y basado en él, escribí un código sencillo de como debería trabajar este pequeño sistema, para luego probar desde interfaz gráfica. Para probar tome en cuenta que se ingresan siempre monedas de un peso y que la tarifa de la máquina es de 5 pesos.


Usando Spin desde interfaz gráfica es posible generar un diagrama desde el código escrito y su ejecución.

Ahora lo mismo, pero modelado como dos tareas independientes, incluyendo las líneas de skip, para uso de exclusión mutua, donde se accede a la variable "x".


Si corremos directo en terminal, podemos observar lo siguiente, que no es más que la ejecución de los dos procesos. Esto es solo una sección, ya que al correr el programa los procesos están en ejecución de forma infinita.

One coin introduced
One coin introduced
One coin introduced
One coin introduced
One coin introduced
    Ticket printed
One coin introduced
One coin introduced
One coin introduced
One coin introduced
One coin introduced
    Ticket printed

Podemos verificar el programa desde interfaz gráfica, y nos dará información acerca de nuestro programa. Nos da información acerca de cuantos estados y transiciones se crearon, si existe error alguno en la ejecución, la cantidad de memoria y procesos creados, etcétera.

Referencias:
[1] - Promela - Definición
Spin on Linux
Promela Model
Model Checking

Redes Petri: Sistema Concurrente

Verificación y Validación de Software
Entrada 8

La entrega para esta semana consistió en lo siguiente:

• Investigar sobre las redes Petri.
• Inventar un pequeño sistema concurrente.
• Modelar un sistema con una red Petri y correrlo en Python.

¿Qué es una red de Petri?

Las redes de Petri son una herramienta gráfica para modelar sistemas formales que pueden ser descritos en términos de pasos en una actividad: como los procedimientos legales, procesos industriales, recetas y algoritmos. Los diseñadores industriales pueden usarlos, ya que son lo suficientemente generales como para la mayoría de los problemas y proporcionan un modelo para la programación. [1]

Una red de Petri es una representación matemática o gráfica de un sistema a eventos discretos en el cual se puede describir la topología de un sistema distribuido, paralelo o concurrente. La red de Petri esencial fue definida en la década de los años 1960 por Carl Adam Petri. Son una generalización de la teoría de autómatas que permite expresar un sistema a eventos concurrentes. [2]

Una red de Petri está formada por lugares, transiciones, arcos dirigidos y marcas o fichas que ocupan posiciones dentro de los lugares. [3]

Las reglas son:

• Los arcos conectan un lugar a una transición así como una transición a un lugar.
• No puede haber arcos entre lugares ni entre transiciones.
• Los lugares contienen un número finito o infinito contable de marcas.
• Las transiciones se disparan, es decir consumen marcas de una posición de inicio y producen marcas en una posición de llegada.
• Una transición está habilitada si tiene marcas en todas sus posiciones de entrada.

Modelar un sistema

El sistema que decidí modelar fue el de las máquinas que hay en las gasolineras, en mi caso hice una versión simple, ya que el sistema completo requiere de más estados y transiciones que las que yo usé.

Lo que tome en cuenta para el sistema fue lo siguiente:

• La máquina se encuentra en reposo hasta que es accionada.
• El personal indica cual es la cantidad de gasolina a expedir.
• Se selecciona el tipo de gasolina, que puede ser la premium o magna.
• La máquina verifica si hay disponible el tipo deseado.
• Si no hay disponibilidad, muestra un mensaje de agotado.
• Si hay disponibilidad, empieza el llenado.
• Al final vuelve al estado de espera nuevamente.

El siguiente es un dibujo creado previo a modelar el sistema en python, y muestra una idea general de como fluye el sistema.

Modelar la Red Petri con Python

Para modelar el sistema en python, fue necesario hacer uso de la librería python-snakes, que es posible descargar desde el siguiente sitio.

Python Snakes

Snakes es una librería de python que nos proporciona todo lo necesario para definir y ejecutar muchos tipos de redes Petri. Su objetivo es tener al alcance una herramienta para crear prototipos rápidamente para nuevas ideas.

Unos de los puntos a resaltar de esta librería es la extensión de plugins, que permite ampliar funciones básicas y trabajar con clases especializadas en redes Petri. Por ejemplo, están los plugins usados para dibujar las redes de Petri en sus diferentes formas y exportarlos como imágenes.

El modelo de la imagen mostrada anteriormente fue escrito con las funciones que python-snakes proporciona, y el código fue el siguiente.


Este código al final crea las diferentes representaciones posibles de la red Petri, aquí deje solo dos de las cinco generadas, que son las que en este caso muestran de una forma más organizada la red.

La siguiente parece más ordenada y es más parecida al modelo del sistema que cree con la herramienta de dibujo.

Recursos consultados:
[1] - Petri Nets
[2] y [3] - Definición de Redes Petri
Python Snakes - Google Code
Python Snakes - API
Franck Pommereau's Blog

Aplicación de la Lógica Predicativa

Verificación y Validación de Software
Entrada 7

La lógica predicativa tiene un amplio rango de aplicaciones, y yo he seleccionado para esta publicación el tema de procesamiento del lenguaje natural.

El procesamiento del lenguaje natural, es un campo que se ha venido desarrollando prácticamente desde los inicios de la informática. Lo que se busca en este campo es hacer preguntas al ordenador y recibir respuestas útiles, o dándole órdenes que la computadora actúe de forma razonable. Por ser una aplicación que hace un tiempo era tal vez muy difícil de imaginar en la realidad, ha aparecido en la ciencia ficción muchas veces.

Actualmente los sistemas encargados del procesamiento del lenguaje natural, han hecho uso de lenguajes de programación con amplia experiencia en este ámbito, como lo es el reconocido uso de Prolog, como un lenguaje lógico que puede llegar a una respuesta al darle una serie de predicados que son ciertos o falsos, en ciertas circunstancias.

¿Cómo es el procesamiento del lenguaje?

Lo que se necesita primeramente para lograr el procesamiento del lenguaje natural es romper el texto capturado como una estructura de oraciones, mediante estructuras lógicas, con el fin de un posterior análisis.

Suele ser difícil la parte del procesamiento, debido a que se tratará con una cantidad grande de información, y esta en base al contexto en que se este hablando, es posible entrar en una serie de ambigüedades que hagan difícil llegar a una solución o resultado.

También el procesamiento depende mucho del lenguaje en el que se aplique, por lo que se suelen utilizar una serie de diccionarios, de los cuáles podamos hacer uso para dar significado lógico a una oración procesada por el sistema.

Pueden ser utilizados para proporcionar retroalimentación auditiva en un sistema automatizado de comprobación de precios en un supermercado o para leer en voz alta una previsión del tiempo que cambia frecuentemente.

El proceso por el que pasa un texto requiere de un análisis que ha de descomponerse en estructuras que el sistema pueda procesar, y luego diferenciarlo en cierto tipo de unidades específicas de información.

La forma de entender como se estructura la entrada de información, es tal y como se hace en la lógica de predicados, de ahí que esta aplicación surge de este tema, ya que se realiza un árbol en el que se estructuran los predicados, hasta llegar a unidades lógicas pequeñas que sea posible evaluar como si fuesen funciones.

La siguiente imagen muestra el procesamiento que hace el sistema al que hace mención el PDF anexado al final de esta publicación como recursos consultados, donde los creadores de el sistema de procesamiento de lenguaje natural utilizan esta misma metodología para analizar la información.

Y ahora es necesario trasladar esas unidades elementales al sistema como si fuesen parámetros a evaluar, una forma de visualizar como se mandaría la entrada de datos al sistema computacional encargado de evaluar la información o texto, se vería de la siguiente manera.

La respuesta de salida, puede determinar si una oración o texto tiene coherencia en cuanto al contexto en el que se estaba hablando, o determinar una serie de acciones a realizar por un sistema.

Recursos consultados:
A Natural Language Interface Using First-Order Logic, Andrews, Itz and Meyer
Logic Predicate - Chapter 4

Escribir Fórmulas con Lógica Predicativa

Verificación y Validación de Software
Entrada 6

Para esta semana hemos seleccionado un ejercicio del Capítulo 4: "The World According to Predicate Logic" del libro llamado "Logic in Action". El enlace al PDF se encuentra al final de esta publicación.

El ejercicio que seleccione trata de escribir la fórmula lógica predicativa de unas oraciones, pero para poder entender que es lo que tenía que hacer, el mismo libro tiene algunos ejemplos, por lo que me gustaría empezar mostrandoles esas oraciones y su respectiva fórmula.

Los ejemplos van desde el uso simple de cuantificadores, hasta las que usan cuantificadores múltiples dentro de la fórmula. Para todos se asume que el dominio son los seres humanos o personas.

Tenemos que:
∀, todos, para todos.
∃, alguien, por lo menos uno, algunos, algunas.
Wx, significa que una persona "x" camina (Walk).
Bx, evalúa si "x" es un niño (Boy).
Gx, evalúa si "x" es una niña (Girl).
Sxy,significa que "x" ve a "y" (Sees).

Después de definir estas fórmulas podemos ver los ejemplos:
Alguien camina: ∃xWx
Algún niño camina: ∃x(Bx ^ Wx)
Una niña ve a John: ∃x(Gx ^ Sxj)
Todos los niños caminan: ∀x(Bx ⇒ Wx)
Alguien ve a todos: ∃x∀ySxy

Después de ver estos ejemplos logre aclarar mi mente y empece a contestar mi ejercicio que es el siguiente.

Ejercicio 4.13
Escribe las siguientes oraciones a fórmulas de lógica de predicados. Suponga que el dominio del discurso son los seres humanos.

Necesitamos una expresión que evalúe si alguien ama a alguien, entonces denotamos Lxy, para una "x" que ama a "y", donde L es abreviación de "Love". Además de B y G, que ya mencione anteriormente que evalúan si se es niño o niña.

1. Algún niño no ama a todas las niñas. (Some boy doesn’t love all girls)

∃x(Bx ^ ∀y(Gy ^ ¬Lxy))

Se evalúa si algún "x" es un niño, y si para toda "y" que resulte ser niña, "x" no ama a toda "y".

2. Todo niño que ama a una niña es también amado por alguna niña. (Every boy who loves a girl is also loved by some girl)

∀x((Bx ^ ∃y(Gy ^ Lxy)) ⇒ ∃z(Gz ^ Lzx))

La primer parte es parecida al anterior, pero ahora se habla de "todo niño" lo que nos hace cambiar el cuantificador, y quitamos la negación en L, porque ahora se dice que el niño ama a la niña. Para la segunda parte se dice que el niño "x" es amado también por una niña, y necesitamos una variable más, porque la niña "y" que el niño "x" ama, puede no ser la misma niña que ama a ese niño "x". Se agrega el signo condicional entre las dos partes, ya que la primer parte implica que la segunda también sea cierta.

3. Toda niña que ama todos los niños no ama a todas las niñas. (Every girl who loves all boys does not love every girl)

∀x((Gx ^ ∀y(By ⇒ Lxy)) ⇒ ∀z(Gz ^ ¬Lzx))

Aquí la primera parte de la oración implica a la segunda, y se traduce como, toda niña "x" que ama a niños "y", entonces niña "y" no ama a niñas "z". Otra forma de entender la oración después de haberla escrito en fórmula lógica, es que si una niña ama a los niños, se sabe que esa niña no ama a las niñas.

4. Ninguna niña quién no ama a un niño ama una niña que ama a un niño. (No girl who does not love a boy loves a girl who loves a boy)

∀x(((Gx ^ ∀w(Bw ^ ¬Lxw)) ^ ∀y(Gy ^ ∃z(Bz ^ Lyz))) ⇒ ¬Lxy)

Gx ^ ∀w(Bw ⇒ ¬Lxw): una niña "x" que no ama a todo niño "w".
Gy ^ ∃z(Bz ^ Lyz): una niña "y" que ama a un niño "z".
¬Lxy: si los dos anteriores se cumplen, entonces la niña "x" no ama a la niña "y", y es ahí donde se aplica la negación que refiere a "ninguna niña" (ninguna niña "x" ama a niña "y").

Páginas consultadas:
The World According to Predicate Logic

Lógica Predicativa

Verificación y Validación de Software
Entrada 5

Para esta semana la tarea es del tema de lógica predictiva, y para esto tenemos un par de enunciados que debemos expresar mediante lógica de predicados y deducir una conlusión.

El ejercicio que yo seleccione es el número 91 de la página 106 del libro "Symbolic Logic" de Lewis Carroll. Al final se encuentra el enlace a la versión en línea del libro.

Los enunciados originales son los siguientes:

All clear explanations are satisfactory.
Some excuses are unsatisfactory.

Y al español las podemos traducir como:

Todas las explicaciones claras son satisfactorias.
Algunas excusas son insatisfactorias.

Las expresiones que usé son las siguientes.

C(x): clear explanations, explicaciones claras
S(x): satisfactory, satisfactorias
E(x): excuses, escusas

Para este caso podemos denotar a x como un comentario cualquiera, y que puede ser evaluado como una explicación o una escusa, o determinar si ese comentario es satisfactorio o no.

Los cuantores usados son los siguientes.

∀: Todos, para todos
∃: Por lo menos uno, algunos, algunas

Ahora vamos a escribir los enunciados con cuantores lógicos y usando las expresiones mencionadas.

Todas las explicaciones claras son satisfactorias.

∀x C(x) ⇒ S(x)

Algunas excusas son insatisfactorias.

∃x E(x) ⇒ ¬S(x)

Ahora podemos usar equivalencias lógicas de los cuantores para poder llegar a la conclusión, e inclusive es fácil hacerlo con sentido común. Podemos entender del segundo enunciado que algunas escusas no son satisfactorias, pero es posible encontrar escusas que son satisfactorias.

Sabemos del primer enunciado que toda explicación clara es satisfactoria, entonces como no todas las excusas son satisfactorias, sabemos que no todas las escusas son explicaciones claras.

La conclusión es:

Algunas excusas no son explicaciones claras.

Lo mismo pero en inglés:

Some excuses are not clear explanations.

Y escrito con expresiones lógicas:

∴ ∃x E(x) ⇒ ¬C(x)

Fuentes consultadas:
Symbolic Logic By Lewis Carroll
Lógica Predictiva - Elisa Schaeffer

Diagrama de Decisión Binario

Verificación y Validación de Software
Entrada 4

¿Qué es un BDD y un ROBDD?

Un Diagrama de Decisión Binario (Binary Decision Diagram o BDD) es un grafo acíclico dirigido con: (a) Uno o dos nodos terminales etiquetados con 0 o 1. (b) Un conjunto de nodos variables con dos hijos. Cada nodo variable está etiquetado con un símbolo proposicional. [1]

Otro término relacionado con los diagramas de decisión son el Diagrama de Decisión Binario Reducido Ordenado (Reduced Ordered Binary Decision Diagram o ROBDD). Una ventaja de un ROBDD es que es único para una función particular y un orden de variables. Esta propiedad es útil por ejemplo en la verificación de funciones de equivalencia. [2]

Reducir un BDD a un ROBDD

Las instrucciones que se nos dieron de tarea para esta publicación, fueron las siguientes.

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.

Expresión Booleana

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

Tabla de verdad

Con la tabla de verdad obtendremos los valores de salida para cada nodo al final del diagrama.

A	B	C	D	[(A∧D) ∧ (¬B∧¬D)] ∨ (B∨C)
0	0	0	0	0
0	0	0	1	0
0	0	1	0	1
0	0	1	1	1
0	1	0	0	1
0	1	0	1	1
0	1	1	0	1
0	1	1	1	1
1	0	0	0	0
1	0	0	1	0
1	0	1	0	1
1	0	1	1	1
1	1	0	0	1
1	1	0	1	1
1	1	1	0	1
1	1	1	1	1

Para no tardar en hacer paso por paso la tabla de verdad, utilice de nuevo el programa en python para obtener la salida final de la tabla de verdad y que ya he usado en las tareas anteriores.


Dibujo del BDD

Ahora dibujamos el diagrama de decisión con las salidas obtenidas en la tabla de verdad.

La reducción la hice por pasos iniciando desde abajo del diagrama. En este caso vemos que las salidas de 0 o 1 en los nodos marcados como D, fueron simplificados dejando solo una salida por cada uno de ellos, ya que eso era posible al tener pares de ceros y unos.

Ahora subiendo al nivel de C, podemos eliminar todas los nodos en D que están repetidos, y las líneas que surgen de C dirigen solo a un nodo D, ya que tiene la misma salida.

Ahora al subir a los nodos B, podemos notar a simple vista que todo los nodos bajo ellos son iguales, por lo que podemos eliminar una rama completa y unir la línea que queda libre en el nodo A hacia el B que dejamos.

Con esto ya tenemos nuestro diagrama de decisión binario reducido y ordenado.

Dibujo del ROBDD

Nota: Las líneas punteadas en el diagrama significan que que el valor que toma el nodo del que sale es un cero, mientras que las líneas continuas son unos. Y las cajas de color naranja es la salida que arroja un cierto camino por el diagrama y que siempre termina en 0 o 1.

Recursos consultados:
[1] - Lógica y Programación - Diagramas de Decisión Binarios - PDF
[2] - Diagrama de Decisión Binario

Aplicaciones de la Lógica Proposicional

Verificación y Validación de Software
Entrada 3

En esta publicación hablaré de una de las aplicaciones de la lógica proposicional, primeramente veremos algunos términos y cosas básicas para entrar en el tema, y después hablaré del caso en específico.

Antes de empezar, cabe mencionar que la lógica proposicional es usada en muchos ámbitos, sobre todo computacionales, por lo que su uso suele ser básico en muchos sistemas. De entre varios usos aplicados que me ha tocado leer en internet son la representación del conocimiento o razonamiento con sentido común, dentro del campo de inteligencia artificial, verificación de propiedades en ingeniería de software, algoritmos de aproximación mediante teoría de la computación, verificación de protocolos criptográficos y diseño de circuitos digitales, entre muchos más.

Lógica proposicional

Definición:
"La lógica proposicional es la parte de la lógica que estudia la formación de proposiciones complejas a partir de proposiciones simples, y la inferencia de proposiciones a partir de proposiciones, pero sin tener en cuenta la estructura interna de las proposiciones más simples." [1]

Sintaxis usada en la lógica proposicional

Variables proposicionales (P): p, q, r, s, t...
(Se puede usar cualquier letra del abecedario, pero normalmente se usan letras a partir de la "p")

Conectivos lógicos: ¬, ∨, ∧, →, ↔
(Los conectivos anteriores suelen ser los que se usan, pero existen simbologías diferentes)

Símbolos de puntuación: (, )
(Se usan paréntesis para separar expresiones y evitar confusión, tal y como se hace en álgebra, y también puede ser usados corchetes y llaves)

Es importante saber que cada variable proposicional es una entidad completa y que no se puede dividir, y que solamente puede tomar uno de dos diferentes valores: verdadero (1) o falso (0).

Tablas de conectivas lógicas

Nombre	Lenguaje natural	Ejemplo	Símbolo
Negación	no	No hace frío	¬
Conjunción	y	Hace frío y está nublado	∧
Disyunción	o	Hace frío o hace calor	∨
Condicional	si-entonces	Si hace frío, entonces uso abrigo	→
Bicondicional	si y sólo si	Está nublado si y sólo si hay nubes visibles	↔

Para cada una de estas conectivas lógicas existen tablas de verdad, que me imagino ya hemos visto en algún momento dentro de nuestras clases, les dejo aquí una imagen con las tablas de verdad de los conectivos anteriores, obtenida de Wikipedia y que compare con algunos apuntes, para verificar que están correctas.

Uso de la lógica en computación

"Debido a que los computadores trabajan con información binaria, la herramienta matemática adecuada para el análisis y diseño de su funcionamiento es el Álgebra de Boole. El Álgebra de Boole fue desarrollada inicialmente para el estudio de la lógica. Hoy en día, esta herramienta resulta fundamental para el desarrollo de los computadores ya que, con su ayuda, el análisis y síntesis de combinaciones complejas de circuitos lógicos puede realizarse con rapidez." [2]

Todo lo anterior son nociones básicas que ya debemos de saber, y es solo una breve introducción, para poder entrar en el caso particular.

Diseño de circuitos

La realización del diseño de un circuito puede involucrar la creación de un sistema electrónico complejo, como el de una placa madre de una computadora, o circuitos menos complejos como el de un sistema integrado.

Cuando son diseños "pequeños" es fácil que una sola persona pueda hacerlos, pero cuando se habla de algo complejo, se requiere a un equipo de personas que hagan un diseño con enfoque sistemático y del cuál se puedan hacer pruebas mediante un simulador, antes de la fabricación del mismo.

La etapa del diseño del circuito, es donde se genera el esquema del circuito integrado, y se considera una etapa media entre el diseño lógico (donde se dice qué debería de hacer el circuito en base a que entradas) y el diseño físico (parte en la que se estructura el diseño del circuito a imprimir a una placa).

[Al hablar de un circuito impreso en una placa me refiero a algo como en la siguiente imagen]

[http://www.arqhys.com/contenidos/diseno-circuitos.html]

Un circuito lógico es aquél que interpreta la información y hace una operación en base a el voltaje de entrada, que puede ser "alto" (1) o "bajo" (0).

El circuito ejecutará una serie de funciones lógicas, a través de puertas lógicas como los conectivos NOT, AND y OR, así como de combinaciones de las mismas como XOR.

Puertas lógicas

En seguida imagen con las puertas lógicas mencionadas. Estas no son todas las existentes.

[http://blogpumaagl.blogspot.mx/2010/10/circuitos-logicos.html]

Como podemos observar cada puerta tiene dos valores de entrada, a excepción del NOT, y solamente pueden tener un valor de salida 0 o 1, y para cada una de ellas existe una tabla de verdad, las mismas que en los conectivos lógicos correspondientes mencionados en la primer parte de esta publicación.

Ejemplo de diseño de un circuito

Para realizar un circuito lo primero que necesitamos es saber las especificaciones del cliente, es decir, saber que es lo que se quiere que el circuito de como resultado.

Enseguida les comparto un ejemplo de mis apuntes de sistemas digitales, donde podemos aplicar el diseño de un circuito.

"Diseñar un circuito que indique al operador de la torre de control de un aeropuerto cuando un avión Jumbo 747 puede aterrizar. Se tienen 3 pistas en el aeropuerto (p, q y r), y cuando una de ellas esta disponible, se obtiene una entrada lógica de 1. Además este tipo de avión solo puede aterrizar cuando existen dos pistas contiguas disponibles."

Ahora sabemos que lo que se desea es un indicador para el operador de la torre, este puede ser un led que encienda cuando es posible aterrizar. Se enciende cuando la salida del circuito es 1, se mantiene apagado cuando la salida es 0. Como entrada tenemos 0 si la pista no esta disponible, y 1 cuando si lo esta.

Creamos una tabla de verdad con las salidas que necesitamos.

p	q	r	Salida
0	0	0	0
0	0	1	0
0	1	0	0
0	1	1	1
1	0	0	0
1	0	1	0
1	1	0	1
1	1	1	1

La tabla queda así, porque solo cuando tenemos dos unos contiguos en las entradas (dos pistas contiguas disponibles), significa que la salida sera 1 (puede aterrizar el Jumbo 747).

Ahora mediante mapas de Karnaugh, obtendremos la proposición de salida.

r \ pq	00	01	11	10
0	0	0	1	0
1	0	1	1	0

Con esto podemos obtener la función lógica del circuito.
S = qr + pq
S = (q^r) ∨ (p^q)

Y el diseño de este circuito usando puertas lógicas quedaría así:

Podemos simplificar:
S = q(r + p)
S = q^(r ∨ p)

[Imágenes creadas desde http://www.circuitlab.com/editor]

Con este circuito podemos dar solución al problema planteado, y básicamente los pasos que seguí son los que se utilizan para el diseño de circuitos.

Verificación y pruebas del diseño de un circuito

"Una vez que el circuito ha sido diseñado, debe ser a la vez verificado y probado. La verificación es el proceso de pasar a través de cada etapa de diseño y asegurando que va a hacer lo que la especificación exige que haga. Esto es frecuentemente un proceso altamente matemático y puede involucrar a gran escala simulaciones por ordenador del diseño. En cualquier diseño complejo que es muy probable que los problemas se encuentran en esta etapa y puede implicar una gran cantidad del trabajo de diseño de hacerse de nuevo con el fin de solucionarlos." [3]

Referencias y documentos consultados:
[1] y [2] Lógica proposicional
[3] Circuit design
Lógica proposicional - PDF
Diseño de circuitos lógicos - PDF

Forma Normal Disyuntiva - DNF

Verificación y Validación de Software
Agregado 1

Como tarea extra realice un ejemplo pequeño de una proposición y que lo pasaré a la forma normal disyuntiva, que se denota por DNF por sus siglas en inglés.

La idea de esto es inventar cualquier proposición, y mediante leyes de equivalencia, como las leyes de Morgan, hagamos que nuestra proposición quede expresada únicamente con los operadores de negación y disyunción, que se denota así {¬, ∨}.

Entonces la proposición simple que invente es.

(¬c → b)^(c → ¬a)

Y ahora vamos a cambiar los operadores usados para que quede, como ya dije, con operadores de negación y disyunción.

Por si tienen duda de las leyes de equivalencia, yo encontré en la siguiente página las más básicas y que me ayudaron en la realización de esta tarea.

Leyes de equivalencia

Entonces tenemos que:

(¬c → b) ^ (c → ¬a)
Primero pasamos a eliminar los operadores condicionales que están dentro de los paréntesis, con la ley de Implicación Material.

(¬¬c ∨ b) ^ (¬c ∨ ¬a)
Simplificamos la parte del doble operador negativo.

(c ∨ b) ^ (¬c ∨ ¬a)
Luego para eliminar la conjunción, usamos las leyes de Morgan.

¬[¬(c ∨ b) ∨ ¬(¬c ∨ ¬a)]

Y ahora ya tenemos la proposición expresada solo con operadores de negación y de disyunción. Ahora vamos a probar si la original, con esta última nos dan como resultado la misma tabla de verdad.

Para ahorrar tiempo use el mismo programa que había creado para verificar si una proposición era una tautología, y probé estas dos proposiciones.


Entonces para (¬c → b) ^ (c → ¬a) el siguiente resultado.

esteban@presario:~/Documents/programas/verificacion$ ./tabla_de_verdad.py 
conjuncion(condicional(negacion(C),B) , condicional(C,negacion(A)))
a b c  S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Y para ¬[¬(c ∨ b) ∨ ¬(¬c ∨ ¬a)] se obtuvo.

esteban@presario:~/Documents/programas/verificacion$ ./tabla_de_verdad.py 
negacion(disyuncion(negacion(disyuncion(C,B)),negacion(disyuncion(negacion(C),negacion(A)))))
a b c S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Y como podemos observar, en las dos tablas de verdad obtenemos los mismos valores en la salida S.

Ahora con mapas de Karnaugh

También es posible obtener la proposición en DNF, mediante códigos de Gray y mapas de Karnaugh.

Para esto partimos de la proposición original (¬c → b) ^ (c → ¬a) y obtenemos sus valores de salida junto con los códigos Gray, en una tabla de verdad.

a b c S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Y ahora usando mapas de Karnaugh obtendremos la forma normal disyuntiva (DNF).

c \ ab	00	01	11	10
0	0	1	1	0
1	1	1	0	0

Y los mapas nos dan la proposición a'c + bc', que podemos escribir también como (¬a^c) ∨ (b^¬c), y en base a la definición de wikipedia de "una fórmula está en forma normal disyuntiva (DNF) si corresponde a una disyunción de cláusulas conjuntivas" [1], sabemos que lo que esta entre paréntesis son las cláusulas conjuntivas, y hay una disyunción entre los dos.

Con el programa volvemos a probar con esta nueva fórmula, y vemos que la tabla de verdad sigue dando los mismos resultados de salida.

esteban@presario:~/Documents/programas/verificacion$ ./tabla_de_verdad.py 
disyuncion(conjuncion(negacion(A),C),conjuncion(B,negacion(C)))
a b c S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Recursos consultados:
[1] Forma normal disyuntiva - Wikipedia
Leyes de equivalencia

Tautología

Verificación y Validación de Software
Entrada 2

¿Qué es una Tautología?

Tautología es una fórmula de un sistema que resulta verdadera para cualquier interpretación. En otras palabras, se trata de una expresión lógica que es verdadera para todos los posibles valores de verdad de sus componentes atómicos.

Determinar si una fórmula es una tautología

Para determinar si una fórmula cualquiera es una tautología, basta con considerar todas las posibles interpretaciones de las fórmulas atómicas, y calcular el valor de verdad del todo. Esto se logra mediante una tabla de verdad.

Tarea

Encontrar por nosotros mismos una fórmula que resulte ser una tautología. Esta debe contener por lo menos 3 variables y 4 conectivos, que pueden ser operadores de negación, disyunción y conjunción.

Solución

La forma en que logre encontrar una tautología fue en un inicio a "prueba y error", ya que lo que estaba haciendo era escribir una fórmula cualquiera, creada con operadores al azar y luego probar mediante una tabla de verdad si esta daba como resultado siempre un valor "verdadero" o 1, pero resultaba ineficiente ya que era tardado probar con las 8 diferentes entradas de valores posibles, representadas en una tabla de verdad.

Entonces para no perder tiempo en verificar cada fórmula creada, decidí hacer un programa en python que me ayudara a verificar más rápidamente si mi fórmula daba verdadero para todas las diferentes y posibles entradas, según una tabla de verdad.

Programa tatutologia.py


Entonces lo que se hace es escribir mediante funciones, en el apartado de la variable formula, los operadores lógicos de la fórmula que se desea probar.

Una de las fórmulas que probé fue la siguiente:
F(A,B,C) = (A|¬B)^(C|¬C)

La cual escrita en el programa cambiaba la variable formula por:
formula = bool(conjuncion(disyuncion(A, negacion(B)) , disyuncion(C, negacion(C))))

Y el resultado que arrojo no fue una tautología ya que en más de una entrada dio como resultado False.

Luego hice unos cambios en la fórmula, y me resulto una tautología, y la fórmula usada fue:
F(A,B,C) = ((A|¬A) | ¬B) ^ (C|¬C)

Cuya fórmula escrita en mi programa es:
formula = bool(conjuncion(disyuncion(disyuncion(A, negacion(A)), negacion(B)) , disyuncion(C, negacion(C))))

Y la captura de pantalla de la ejecución donde se muestra que para la tabla de verdad dada, siempre da como resultado un True.

Árbol

P = ((A|¬A) | ¬B) ^ (C|¬C)

Tabla de verdad

Para comprobar con la tabla de verdad que todos los valores dan Verdadero, hacemos paso por paso, tal y como se desglosa en el árbol y vemos que obtenemos como resultado en la última columna los valores de 1 o Verdadero.

Nota: En el programa mostrado también se incluyeron funciones para comprobar fórmulas donde se incluyen el operador condicional y bicondicional, pero solo fueron para probar algunos ejemplos de tautologías encontradas en internet, y así verificar que el programa estaba haciendo lo correcto.

Referencias:
Definición de Tautología

¿Qué es la Verificación y Validación de Software?

Verificación y Validación de Software
Entrada 1

Es un 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.

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.

Los atributos de la calidad deben ser la corrección, la perfección, la consistencia, la confiabilidad, la utilidad, la eficacia, el apego a los estándares y la eficacia de los costos totales.

Hay dos tipos de verificación: formal y del ciclo de vida. Esta última consiste en el proceso de determinar el grado de los productos de trabajo de una fase dada del ciclo de desarrollo cumplen con las especificaciones establecidas durante las fases previas. La verificación formal es una rigurosa demostración matemática de la concordancia del código fuente con sus especificaciones.

La validación es la evaluación del software al final del proceso de desarrollo del software para determinar su conformidad con los requisitos IEEE.

La verificación y validación implican la valoración de los productos de trabajo para determinar el apego a las especificaciones, incluyen las especificaciones de requisitos, la documentación del diseño, diversos principios generales de estilo, estándares del lenguaje de instrumentación, estándares del proyecto, estándares organizacionales y expectativas del usuario, al igual que las meta especificaciones para los formatos y notaciones utilizadas en la especificación de productos diversos.

¿Qué es verificación?

La verificación se enfoca más al proceso de evaluación del sistema o componentes ya que permite determinar si los productos de una determinada fase del desarrollo satisfacen las condiciones impuestas en el inicio de la etapa.

¿Qué se debe tener en la verificación?

• Consistencia: vigilar que la información sea coherente.
• Precisión: corrección de la sintaxis.
• Completitud: lagunas en capacidad deductiva.

Lo que se hace en la verificación:

• Identifica desviaciones con estándares y requerimientos.
• Recolecta datos para mejorar el proceso.
• Verifica que el producto:
  - Cumpla con los requerimientos.
  - Cumpla con los atributos de calidad.
  - Se ajuste a las regulaciones, estándares y procedimientos definidos.
  

¿Qué es validación?

La validación también es una evaluación del sistema o de componentes, solo que es en el transcurso o al final del proceso del desarrollo, donde se determina si cumple con lo especificado.

Aspectos en la validación:

• Construir el sistema correcto.
• Evaluar la conformidad con la especificación de requisitos.

Métodos formales de verificación

Entre los métodos de verificación más utilizados, se encuentran:

• Aserciones E/S: El programa, en lógica de Hoare, se especifica mediante aserciones que relacionan las entradas y salidas del programa. Se garantiza que si la entrada actual satisface las restricciones de entrada (precondiciones) la salida satisface las restricciones de salida (poscondiciones).
• Precondición más débil: Consiste en dada una poscondición POST, encontrar, operando hacia atrás, un programa S tal que la precondición se satisfaga en un amplio conjunto de situaciones.
• Inducción estructural: La inducción estructural es una técnica de verificación formal que se basa en el principio de inducción matemática.

Ejemplos de grandes pérdidas por errores de software

El desorbitado Mars Climate en 1998

Después de un viaje de 286 días desde la tierra, la nave "Mars Climate Orbiter" encendió sus motores para ponerse en órbita alrededor de Marte. Al llegar a Marte, la sonda debía modificar su trayectoria y reducir su velocidad, de forma que se mantuviera orbitando alrededor del planeta. Los motores arrancaron, pero el ingenio entró demasiado en la atmósfera del planeta, provocando que se estrellara en su superficie.

La causa fue que el software que controlaba los propulsores del Mars Orbiter usaban unidades imperiales (libras de fuerza) en lugar de unidades métricas (Newtons), como especificaba la NASA.

Pérdida: 125 millones de dólares.

Apagón de 2003 en Norteamérica

Privó de electricidad a un estimado de 50 millones de personas. El apagón se debió a un error en el software de monitoreo basado en Unix de General Electric, que impidió que los operadores se dieran cuenta de un corte local de energía. El efecto dominó de la falla afectó a ocho estados de Estados Unidos y a Ontario, en Canadá.

Problema del año 2000

El problema del año 2000, también conocido como efecto 2000 o por el numerónimo Y2K, es un bug o error de software causado por la costumbre que habían adoptado los programadores de omitir la centuria en el año para el almacenamiento de fechas, asumiendo que el software sólo funcionaría durante los años cuyos nombres comenzaran con 19. Lo anterior tendría como consecuencia que después del 31 de diciembre de 1999, sería el 1 de enero de 1900 en vez de 1 de enero de 2000.

Por ejemplo los programas que cuentan el número de años a través de la sustracción de las fechas, obtendrían una cantidad de años negativa. Si una persona nació en 1977, la edad de esta persona en 2000 sería: 00-77 = -77 años.

Y relacionado con este último ejemplo les dejo la primer parte del capítulo de Dilbert donde se enfrentan al problema del año 2000.

Fuentes consultadas:
Introducción a la verificación y validación
Métodos formales
Los errores informáticos más costosos
Problema del año 2000