[VERIFICACIÓN Y VALIDACIÓN] Expresión ω-regular

Esta semana se encargó hacer una expresión ω-regular con almenos 2 simbolos y dos operadores y despues dibujar un NBA de la expresión.

Hice la siguiente expresión:

 Y su NBA es el que sigue:

Referencias:

Link 1
Link 2
Link 3

[VERIFICACIÓN Y VALIDACIÓN] Redes de Petri

Para esta semana se nos encargó modelar un sistema concurrente, en este caso una red de petri. Segun Wikipedia: "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."

En mi caso modelaré el funcionamiento básico de un cajero automático. Para ello tengo que definir los estádos de la máquina y las transiciones entre estados.

Para poder definir los estados y transiciones definire en palabras simples como actua la máquina:

• El cajero se encuentra en espera de que se introduzca una tarjeta.
• Una vez introducida se procede a pedir el NIP.
• Si el NIP es incorrecto se le vuelve a pedir, de ser correcto entonces continua.
• La siguiente es la pantalla de transacciones donde se elige el tipo de transacción (efectivo, cheques, etc).
• Se procede a la selección de cantidad para la transacción.
• Se realiza la transaccion en la que se entrega el efectivo, el tiquet, etc.
• Se pregunta al usuario si desea realizar otra transacción, de ser así se regresa a la pantalla de selección de tipo de transacción, de no ser así se regresa al estado de espera.

Código utilizado usando la libreria de python snakes: Una imagen de como queda finalmente:

Referencias:

Wikipedia

Libro

[VERIFICACIÓN Y VALIDACIÓN] Aplicaciones de la Lógica Predicativa

Un pequeño resumen de lo que trata la lógica predicativa:

La lógica predicativa está basada en la idea de las sentencias realmente expresan relaciones entre objetos, así como también cualidades y atributos de tales objetos. Los objetos pueden ser personas, objetos físicos, o conceptos. Tales cualidades, relaciones o atributos, se denominan predicados. Los objetos se conocen como argumentos o términos del predicado. 

Al igual que las proposiciones, los predicados tienen un valor de veracidad, pero a diferencia de las preposiciones, su valor de veracidad, depende de sus términos. Es decir, un predicado puede ser verdadero para un conjunto de términos, pero falso para otro.

Con esto queda claro el fin de esta, y de esta manera paso a explicar el tema que elegí (me eligieron) para esta tarea: Detección de fallos en automóviles.

ECU

La mayoría de los automóviles en la actualidad tienen un dispositivo que se encarga de checar el buen funcionamiento del vehículo, conocido como "la computadora" que en realidad no es más que un circuito llamado ECU (Engine Control Unit) que controlan generalmente 4 cosas:

• Control de inyección de combustible.
• Control de tiempo de inyección.
• Control de la distribución de válvulas.
• Control de arranque.

Otros dispositivos y sensores conectados al ECU informan sobre otros posibles problemas que pueda haber en el vehículo.

Cuando hay un fallo mecánico, este es informado a la ECU y típicamente prende el "check engine" que indica que algo está mal. El fallo es guardado en la memoria del ECU para un futuro uso.

Muchos mecánicos ofrecen un servicio de diagnóstico por computadora para una mejor revisada, es más efectivo que sacar el motor del vehículo. El software para el chequeo utiliza un mecanismo similar a la lógica predicativa, comparando los valores dados por el ECU con los que vienen de fábrica.

Un ejemplo es cuando las revoluciones por segundo del motor no son las óptimas, ECU se encarga de comparar las revoluciones por segundo que deben existir dentro de un rango, dependiendo de la velocidad a la que se encuentre el vehículo. Si el vehículo muestra un desempeño más bajo al del rango normal, la luz del "check engine" se encenderá.

Otro ejemplo es el bombeo de gasolina, ECU cuenta con un sensor que le permite verificar la cantidad necesaria de aire que se hace pasar por el motor en base a la aceleración del vehículo y de esa manera permitir una mayor o menor cantidad de gasolina. Cuando hay un problema en el bombeo de gasolina, ECU regula la cantidad de aire y gasolina para evitar el calentamiento del motor y evitar fallos severos.

En vehiculos deportivos como los de F1 es crucial este dispositivo, ya que podrian salvar la vida del piloto en casos como algun pistón en mal funcionamiento o mala inyección, cosas que pueden sobrecalentar el motor. En estos vehiculos los ECU detectan fallos en tiempo real, aunque en la actualidad ya muchos lo hacen, lo que significa que si chocan con algun competidor, ECU detecta el problema para que el los ingenieros puedan reparar si es posible el daño en el Pit stop, o bien apaga el vehículo para evitar una posible catastrofe.

[VERIFICACIÓN Y VALIDACIÓN] Lógica predicativa 2

Esta vez se nos encargó realizar un ejercicio del documento proporcionado en clase, del cual yo escogí el siguiente:

Rephrase “x ≤ y ^ y ≤ z” in predicate logic, using binary relations < for “less than” and = for “equal”.

Reformule “x ≤ y ^ y ≤ z” en lógica predicativa, usando relaciones binarias < para "menor que" y = para "igual".

La expresión es:

x ≤ y ^ y ≤ z

Y dice que "x" es menor o igual a "y", y que "y" es menor o igual a "z".

Por lo que quedan las siguientes relaciones binarias:
(x < y), (x = y), (y < z), (y = z)

Al unirlas según la expresión se pueden escribir de la siguiente manera:

[(x < y) v (x = y)] ^ [(y < z) v (y = z)]

O de la siguiente manera:

[(x < y) ^ (y < z)] v [(x = y) ^ (y = z)]

Y de estas podemos reordenarlas de la siguiente manera:

(x < y < z) v (x = y = z)

O bien:

x ≤ y ≤ z

[VERIFICACIÓN Y VALIDACIÓN] Lógica predicativa

Para esta tarea, nos tocó seleccionar una proposición del libro Symbolic Logic de Lewis Carroll.

Yo seleccioné la siguiente:

"All soldiers march well;

Some babies are not soldiers"

La traducción directa es "Todos los soldados marchan bien; Algunos bebés no son soldados".

Ahora hay que expresar lo anterior en terminos de lógica predicativa usando cuantificadores.

∀ - Es el cuantificador universal. Una proposición es universal cuando el concepto o clase que constituye su sujeto está considerado en toda su extensión.

∃ - Es el cuantificador existencial. Una proposición es existencial cuando el concepto o clase que constituye su sujeto está considerado en parte de su extensión.

Analizando la sentencia, podemos definir cada parte de la siguiente manera:

S(x) - Son aquellos que son soldados.
M(x) - Son aquellos que marchan bien.
B(x) - Son aquellos que son bebés.
x - Es alguien.

Ahora podemos escribir:

∀x S(x) → M(x)

"Todo soldado marcha bien"

∃x B(x) → (¬S(x))

"Algunos bebés no son soldados"

Con esto podemos definir otras formas de escribir la sentencia:

∃x B(x) → (¬M(x))

"Algunos bebés no marchan bien"

∃x M(x) → B(x)

"Algunos que marchan bien son bebés"

∃x B(x)M(x) → S(x)

"Algunos bebés que marchan bien son soldados"

∀x S(x) → B(x)M(x)

"Todos los soldados son bebés que marchan bien"

[VERIFICACIÓN Y VALIDACIÓN] Diagrama de Decisión Binario

Se encargó para esta entrada:

• Inventar una expresión Booleana.
• Usando por mínimo 3 variables y 4 conectivos básicos.
• Construir y dibujar el BDD.
• Reducir el BDD resultante a un ROBDD. 
• Dibujar el ROBDD resultante.

Primero iniciamos con la expresión booleana, utilizé la siguiente:

Y esta es la tabla de verdad:

El arbol binario de desición queda de la siguiente manera:

Las lineas punteadas marcan falso y las otras verdadero, quitare los valores para mejor visualización.

Si observamos, las B que son verdaderas son iguales, ya que en ambos casos, la C es verdadera o falsa, así que juntamos ambas. Ahóra reducire el arbol a un BDD (Diagrama de Desición Binario):

El siguiente paso es dejar todo unido a un par de nodos 0 y 1:

Y finalmente, ya que en B falsa, los valores de C pueden ser o verdaderos o falsos, eliminamos las C de los falsos de B y las unimos directamente a los nodos que apuntaban:

[VERIFICACIÓN Y VALIDACIÓN] Lógica proposicional

Para la tarea de esta semana se encargó buscar ejemplos de las aplicaciones de la lógica proposicional en la vida real.

En si, la lógica proposicional estudia las proposiciones o sentencias lógicas, sus posibles evaluaciones de verdad y en el caso ideal, su nivel absoluto de verdad.

Se define una proposición como un enunciado declarativo que puede ser verdadero o falso, pero no ambos a la vez.

Sintaxis

• Constantes lógicas verdadero (V) o falso (F).
• Variables P, Q y R.
• Conectivos lógicos: negación (¬), conjunción (^), disyunción (v), implicación (-->), implicación doble (<-->), etc.
• Símbolos de puntuación: paréntesis ( ), corchetes [ ] y llaves { }.

Tabla de verdad de algunos conectivos lógicos:

Aplicaciones

En matemáticas:

• Fundamenta las matemáticas.
• Rama de las matemáticas.
• Mecanización del razonamiento matemático.

En informática:

• Base de partes de la informática con mayor futuro:
• I.A., Sistemas expertos, 
• Programación Lógica.
• Primer ejemplo de construcción de un lenguaje formal o artificial.
• Paradigma de programación.
• Otras aplicaciones:
• Especificación y verificación de programas.
• Deducción automática.
• Diseño de circuitos electrónicos.

En I.A.

Una visión muy frecuente entre los investigadores de la Inteligencia Artificial es que para que un sistema sea "inteligente", debe contener un componente que se puede entender como lingüístico tal que:

• Contiene el conocimiento del sistema, y
• Conduce el comportamiento inteligente del sistema

Un Agente Basado en Conocimiento (ABC) es aquel sistema que posee conocimiento de su mundo y que es capaz de razonar sobre las posibles acciones que puede tomar para cambiar el estado de su mundo. Mediante sentencias lógicas se logra el razoamiento en conjunto con su conocimiento para dar respuestas lógicas, o bien realizar cambios esperados en algún sistema.

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.

La semántica estudia el significado de los signos lingüísticos, esto es, palabras, expresiones y oraciones. Qué signos existen y cuáles son los que poseen significación esto es, qué significan para los hablantes, cómo los designan, y por último, cómo los interpretan los oyentes.

Teoría : Reglas para inferir oraciones desde otras oraciones

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

En Sistemas Expertos

Los sistemas expertos son programas que reproducen el proceso intelectual de un experto humano en un campo particular, Estos sistemas permiten la creación de máquinas que razonan como el hombre, restringiéndose a un espacio de conocimientos limitado.

Estos sistemas se diferencian de las IA's en que se especializan en un campo muy específico, por lo tanto es eficiente para lo que se diseña, es rápido y puede trabajar en ambientes peligrosos.

Un Sistema Experto está conformado por:

• Base de conocimientos (BC): Contiene conocimiento modelado extraído del diálogo con un experto.
• Base de hechos (Memoria de trabajo): contiene los hechos sobre un problema que se ha descubierto durante el análisis.
• Motor de inferencia: Modela el proceso de razonamiento humano.
• Módulos de justificación: Explica el razonamiento utilizado por el sistema para llegar a una determinada conclusión.
• Interfaz de usuario: es la interacción entre el SE y el usuario, y se realiza mediante el lenguaje natural.

Utilizando una representación primitiva del lenguaje, permite representar y manipular aserciones sobre el mundo que nos rodea.

Mediante la lógica proposicional evalúa sentencias simples, que en conjunto se convierten en unas más complejas, con esta serie de sentencias el sistema es capaz de interactuar con su entorno para adquirir conocimiento o dar la respuesta requerida. A pesar de lo anterior, los sistemas expertos no tienen sentido común desarrollado, osea que no diferencian entre lo que es lógico o ilógico en la mayoría de los casos, a menos que se defina una sentencia para cada caso.

Fuentes

Lógica de proposiciones.

Logica propocicional en I.A.

Lógica Proposicional para Informática.

Sistemas Expertos.

Wikipedia - Conectiva Lógica.

[VERIFICACIÓN Y VALIDACIÓN] Lógica proposicional; formas normales

Para esta tarea buscaré una expresión que sea una tautología.

En lógica, una tautología es una fórmula bien formada de un sistema de lógica proposicional que resulta verdadera para cualquier interpretación; es decir, para cualquier asignación de valores de verdad que se haga a sus fórmulas atómicas. La construcción de una tabla de verdad es un método efectivo para determinar si una fórmula cualquiera es una tautología o no.

Comenzé con una pequeña expresión y trate de que todos sus valores sean verdaderos, la expresión con la que encontré la tautología es la siguiente:

[(A Λ B) Λ C] 

Y esta es la tabla de verdad:

Despues busqué una segunda expresión:

(C V ¬A) V ¬C

Y su tabla de verdad:

Y una ultima expresión:

¬(A Λ ¬B)

Y su tabla de verdad:

Las primeras 2 las uní con un "or", en si esta ya es una tautología:

{[(A Λ B) Λ C] V [(C V ¬A) V ¬C]}

Y su tabla de verdad:

Y esa expresión la uní a la última con otro "or":

{[(A Λ B) Λ C] V [(C V ¬A) V ¬C]} V ¬(A Λ ¬B)

Y la tabla resultante es una tautología.

Por último mencionar que si tenemos una ecuación larga, si alguna de sus expresiones es una tautología, es más facil que toda la ecuación sea una tautología.

http://turner.faculty.swau.edu/mathematics/materialslibrary/truth para las tablas de verdad

[VERIFICACIÓN Y VALIDACIÓN] Introducción a la verificación formal

La verificación y validación es el nombre que se da a los 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.

Verificación:

El papel de la verificación comprende comprobar que el software está de acuerdo con su especificación. Se comprueba que el sistema cumple los requerimientos funcionales y no funcionales que se le han especificado.

Validación:

La validación es un proceso mas general. Se debe asegurar que el software cumple las expectativas del cliente. Va mas allá de comprobar si el sistema está acorde con su especificación, para probar que el software hace lo que el usuario espera a diferencia de lo que se ha especificado.

Los problemas que puede causar el no realizar una verificación y validación han provocado errores fatales tales como:

• Un sistema de alertas, casi causa la 3ª Guerra Mundial (1983). Según el registro del fallido sistema, Estados Unidos había disparado 5 misiles. De no ser por Stanislav Petrov muchas personas habrían muerto y el rumbo de la historia habría cambiado.

• La red de AT&T se colapsa (1990). Durante 9 horas, 75 millones de llamadas no se contestaron en Estados Unidos por un error en la actualización de un software utilizado en el sistema.

• La explosión del Ariane 5 (1996). El cohete -de 8 mil millones de dólares-, que contenía 4 satélites valorados en 500 millones de dólares, explotó tras sufrir un fallo en su computador: el aparato saltó en pedazos a los 36,7 segundos de su lanzamiento, al tratar de convertir unos datos de formato 64 bits a formato 16 bits.

• El Airbus A380 se retrasa por problemas de incompatibilidad de software (2006). Los aviones se hacen por partes, así que una hecha en Alemania se hizo con una versión desactualizada de un programa, mientras que en la otra -hecha en Francia- se utilizó la versión más reciente de dicho software. Hubo problemas al tratar de conectar ambas partes y el lanzamiento comercial y la producción de los aviones se retrasó un año.

• El Mars Climate Observer se estrella por el sistema métrico (1998). Se perdió una nave de 125 millones de dólares que iba a estudiar el clima de Marte, cuando hubo un fallo en el cálculo de aterrizaje y terminó por quemarse en la atmósfera. El problema fue que una compañía subcontratada por la NASA utilizó el sistema anglosajón en lugar del sistema métrico decimal, normalmente utilizado por la agencia.

• EDS y la Agencia de Ayuda a la Infancia (2004). La reforma de la agencia y el programa diseñado por EDS se convirtieron en un verdadero dolor de cabeza para la administración y para los presupuestos de la institución: para remediar los errores, se estaban gastando 70 céntimos por cada libra que entraba.

• El Y2K (2000). Todo el mundo esperaba el caos cuando millones de ordenadores en el mundo no pudieran procesar los dígitos del nuevo año. Fue muchísimo dinero el que perdieron las empresas, cuando finalmente llegaron las 12 del 1/1/2000 y las máquinas desactualizadas no causaron la catástrofe.

• La explosión de los portátiles (2006). El primero fue marca Dell y aprovechó un momento inoportuno -una feria japonesa-. Fue un problema en la batería que provocó que la compañía hiciera un recall de 4,1 millones de baterías. Pero en la saga le siguieron Matsushita, Sony, Lenovo, Acer e incluso Apple. ¡Boom!

• Siemmens y los pasaportes ingleses (1999). Se unieron 2 causas: por primera vez, los menores de 16 años necesitaban pasaporte para viajar, y la agencia encargada de emitirlos empezó a utilizar un sistema que no se probó lo suficiente.

• Se colapsa el Aeropuerto de Los Angeles (2007). Unas 17 mil personas se quedaron en tierra por un problema de software que provocó conflictos en una tarjeta de red que no funcionó como debía y tiraba de toda la red informática.

Fuente - ALT1040.com