Mostrando entradas con la etiqueta Verificación y Validación de Software. Mostrar todas las entradas
Mostrando entradas con la etiqueta Verificación y Validación de Software. Mostrar todas las entradas

martes, 13 de noviembre de 2012

Lineal Temporal Login (LTL)

La lógica temporal es parte de la lógica modal, la cual se utiliza en sistema de reglas donde se presenta el tiempo. 

En lógica temporal se encuentran los mismos operadores que en la lógica de primer orden, agregando algunos más entre los que se encuentran: siempre, algunas veces, nunca. 

Algunos sistemas lógicos que se basan en lógica temporal son: Lógica computacional en árbol (CTL), lógica linear temporal (LTL) y Lógica temporal de intervalos (ITL).

La lógica temporal cuenta con dos tipos de operadores: operadores lógicos y operadores modales. Los operadores modales usan el Linear Temporal Logic y Computation Tree Logic. En la siguiente tabla se muestran estos operadores y su explicación.


Fuente: Wikipedia

Para esta tarea, se nos pidió elegir un problema del siguiente link: http://www.voronkov.com/lics_doc.cgi?what=chapter&n=14 

Me tocó el número 3 de los ejercicios 14.2:

If A holds at a state i, then B must holds at at least one just after i.

Entonces podemos decir que:

Siempre que A se mantenga en un estado i, debe estar B eventualmente.

Referencias:




martes, 6 de noviembre de 2012

Propiedades de modelos de verificación

Para esta semana la tarea es inventar una expresión regular y dibujar su NBA (Nondeterministic Büchi Automata).

Las expresiones regulares describen las combinaciones de caracteres en el texto, se puede definir como un conjunto de caracteres que forman un patrón, que representan a otro grupo de caracteres mayor, de forma que se pueda comparar el patrón con otros conjuntos de caracteres para ver las coincidencias. 

En la tabla siguiente se muestran algunos de los símbolos que se utilizan y lo que significa cada uno de ellos.



Entonces, como dijimos una expresión regular consiste en comprar un patrón con un texto para ver si el texto contiene dicho patrón.

Por ejemplo:

Patrón: Mi
- Miguel
- Camión
- Mimi

Patron: [mp] adre
-Madre
-Padre

Sintáxis y caracteres

El punto

Representa cualquier carácter, escribir un punto en un patrón significa que hay un carácter, cualquiera. Desde la A a la Z (mayúscula o minúscula), del 0 al 9, o algún otro símbolo.

Ejemplo:
pa.a coincide con pasa, pata, para, paja, etc. NO coincide: pasta ni paa.

Principio y fin de cadena

Si se quiere indicar que es el principio de la cadena o que es el final, se utiliza ^para inicio y $ para final.

Ejemplo:
^pájaros coincide con "pájaros amarillos", pero no con "bonitos pájaros"
$rosa coincide con "color rosa" 

Cuantificadores

Se utilizan para indicar que algún elemento del patrón se repetirá un número intedeterminado de veces, se utiliza "*" o "+". Usando "+" para decir que el elemento anterior aparece uno o más veces, y con "*" decimos que el elemento anterior aparece cero o más veces.

Por ejemplo:
"casa+" coincide con "casaa" "casaaa" "casaaaa", etc. 
"ab*c" coincide con "ac" "abc" "abbc" "abbbc", etc.

Si se quiere indicar un elemento que puede que esté (una vez) o puede que no esté se utiliza "?".

Se puede definir la cantidad de veces que se va a repetir, para esto se utilizan las llaves     "{ }".

Ejemplo:
abc{1,2} coincide con "abc" "abcc"


Mi expresión regular es la siguiente:



En esta expresión podemos ver que tiene un operador OR y uno AND, también cuenta con símbolos de los que observamos en la tabla anterior. El símbolo * significa que el carácter anterior se encuentra cero o más veces. 

El NBA correspondiente de esta expresión es el siguiente:






martes, 30 de octubre de 2012

Sistemas de Transiciones

Sistema: 

Elevador

Componentes del sistema: 
  • Elevador: máquina que se encarga de ascender o descender para transportar a la persona de un piso a otro.
  • Botones de subir/bajar: se encargan de mandar una señal para saber si el elevador va a ascender o descender.
  • Persona: es la persona que utiliza el elevador, para subir o bajar a otro piso. Presiona el botón de ascender o descender.
Cada componente cuenta con estados y acciones.

Elevador

Estados:
  • En espera: cuando espera a que la persona presione el botón de subir o bajar.
  • En funcionamiento: se dirige al piso donde se encuentra la persona que presionó el botón y cuando la persona se sube se dirige al piso que la persona desee.
  • Detención: cuando el elevador se detiene en el piso que presiona la persona.
Transiciones:

  • Recibir señal: recibe la señal para dirigirse al lugar donde se encuentra la persona que presiono el botón de Subir/Bajar
  • Subir/Bajar: subir o bajar al piso donde se encuentra la persona que presiono el botón  y posteriormente a donde quiere llegar.
  • Llegar: llevar a la persona al piso donde desea ir y detenerse.



Posición del elevador:

Estados:
  • Arriba: Manda señal al elevador diciendo que va a ascender.
  • Abajo: Manda señal al elevador diciendo que va a descender.
Transiciones:
  • Ascender: si la persona presiona el botón de subir, el elevador sube/baja a donde se encuentre la persona y asciende al piso deseado.
  • Descender: si la persona presiona el botón de subir, el elevador sube/baja a donde se encuentre la persona y desciende al piso deseado.

Persona

Estados:
  • Inicio: cuando presiona el botón de subir o bajar.
  • Espera: cuando espera a que el elevador llegue a donde se encuentra.
Transiciones:
  • Presionar botón Subir/Bajar: cuando la persona llega a un elevador y presiona el botón de subir o bajar.
  • Subir/Bajar del elevador: entra al elevador y presiona el botón del piso a donde desea ir o sale en el piso deseado. 


Se realiza un diagrama de transición para ver el comportamiento del sistema en conjunto.
Elevador || Botones || Persona

Estados:
Componente Elevador: A, B, C (detención, espera, en funcionamiento)
Componente Persona: 0, 1(inicio, espera)
Componente Posición del elevador: 0, 1 (arriba, abajo)


Transiciones:
1, 2, 3, 4, 5 (presionar botón, recibir señal, subir, bajar, llegar)


Este diagrama representa el sistema del elevador.

Referencias:
Libro Principles of Model Checking, Christel Baier & Joost-Pieter Katoen.



lunes, 15 de octubre de 2012

Análisis de fiabilidad

Para esta tarea se nos pidió buscar una aplicación de lógica predicativa, yo elegí el análisis de fiabilidad de sistemas mediante árboles de fallo.

Árbol de fallo.
Es un método gráfico de análisis de riesgo que tiene como objetivo es conocer los modos de daño y las circunstancias que llevan a un fallo crítico de un sistema.

El análisis mediante árbol de fallos (FTA) se utilza para describir como un mecanismo de degradación puede conducir a un modo de fallo.


Esta basado en un razonamiento deductivo, se tiene una falla y se intenta descubrir todos las posibles circunstancias de funcionamiento del sistema que contribuyen a dicha falla.

¿Qué puede hacerse con un análisis de un árbol de fallo?

  • Identificar las causas que pueden provocar el fallo crítico.
  • Repartir la probabilidad del fallo entre estados o circunstancias de niveles abajo.
  • Identificar caminos hacia el fallo crítico y los puntos débiles del diseño para así buscar acciones para corregirlo.
  • Determinar que factores afectan más a la fiabilidad del sistema, así como las modificaciones que se requieran para mejorar esta fiabilidad.
  • Evaluar las diferentes acciones de mejora.
  • Determinar si la fiabilidad del sistema cumple con el requisito.
  • Identificar fallos de causa parecidos.
  • Comparar configuraciones de diseño alternativas.
Metodología para el análisis de fiabilidad mediante Árbol de Fallo.

1. Conocimiento y definición del sistema:
  • Dibujar los diagramas de bloques funcionales y de fiabilidad del sistema
  • Definir el campo de aplicación del análisis
  • Definir el fallo que quiere analizarse 
2. Construcción del árbol de fallo:
  • Identificar los posibles sucesos y causas (sobre el diagrama de bloques) que conducen al fallo que se analiza.
  • Relacionar los sucesos y causas que se identificaron mediante símbolos lógicos, haciendo con esto que se pueda descubrir los caminos lógicos que conduzcan al fallo.
  • Determinar el tipo de cada modo de fallo: primario, secundario o impuesto.
3. Evaluación cualitativa y cuantitativa del árbol de fallo:

Fallo. El árbol de fallo es un modelo cualitativo (lógico) que puede evaluarse cuantitativamente (numericamente).

Este método se utiliza normalmente por instalaciones nucleares, aeronáuticas y espaciales, así como también en la evaluación de riesgos de otras industrias como la química, electrónica, petroquímica, etc.



Para que el árbol de fallos sea eficaz, debe elaborarse por personas profundamente conocedoras de la instalación o proceso de analizar y que también conozcan el método y tengan experiencia en él. 

Los árboles de fallos también se utilizan para evaluar la probabilidad de fallo en sistemas y componentes en donde la probabilidad de fallo es una combinación de varios factores. Debido a esto, la explotación de un árbol de fallos se puede limitar a un tratamiento cualitativo o extenderse hasta una cuantificación de probabilidades de ocurrencia del evento estudiado.


Ejemplo de árbol de fallos para un sistema de bombeo de agua:







Referencias:

lunes, 17 de septiembre de 2012

Lógica Predictiva

Para esta tarea cada uno eligió un problema de un documento que se encuentra en el siguiente enlace. 
The World According to Predicate Logic

El problema que elegí fue el siguiente:

Exercise 4.2 Express ¬(x < y < z) in terms of the binary predicate < and propositional connectives, using the fact that x < y < z is an abbreviation of x < y ^ y < z.



Expresa ¬(x < y < z) en términos de predicados binario < (menor que) y conectivos proposicionales, usando el hecho que x < y < z es una abreviación de x < y ^ y < z.

Para empezar podemos decir que:

La expresión ¬(x < y < z) nos dice que "No es cierto que Y es mayor a X y Y es menor que Z", o sea Y no se encuentra en el rango que hay de X a Z.

Para realizar este ejercicio tenemos que realizar predicados binarios, esto quiere decir que tener dos parámetros en cada expresión y también agregar conectivos lógicos. Para esto podemos decir que:

Predicados binarios con conectivos lógicos:

¬[(x
ó
(y<=x) ^ (z<=y)

Este último se puede expresar también de la siguiente manera:

(x>y>z) v (x=y=z)


martes, 11 de septiembre de 2012

Lógica Predictiva


Para esta semana, se nos dio a elegir unas sentencias y trabajaremos con lógica predictiva.


Las sentencias que elegí fueron.



"No pigs can fly;
All pigs are greedy."

"Ningún cerdo puede volar
Todos los cerdos son codiciosos"


Para esto se definen equivalencias:
P(x) = Cerdo
F(x) = Vuela
G(x) = Codicioso


Combinando los conectivos con los predicados, constantes, variables y los cuantificadores, pueden crearse estas sentencias.

Cuantificadores.

∃x = Por lo menos uno
∀x = Todos

Formulación de expresiones

Ningún cerdo puede volar

¬∃x P(x) ⇒ F(x)

Todos los cerdos son codiciosos

∀x P(x) ⇒ G(x)

Con esto podemos decir que:

Los cerdos son codiciosos y no pueden volar

∴∀x P(x) ⇒ (G(x)^¬F(x))


Referencias

lunes, 3 de septiembre de 2012

Diagrama de decisión binario

Para esta tarea se nos pidió lo siguiente
  • Inventar una expresión Booleana (utilizando por mínimo 3 variables y 4 conectivos básicos).
  • Construir y dibujar su BDD.
  • Reducir el BDD resultante a un ROBDD.
  • Dibujar el ROBDD resultante.
La expresión que invente es la siguiente:

(p ^ q) v (q -> r) ^ (p v ¬r)

Tabla de verdad:



Árbol binario de decisión:



Reducir a ROBDD

Para reducir un árbol binario de decisión a un Diagrama Binario de Decisión se tienen que considerar dos reglas:
  1. Unir los isomorfismos (de igual forma) de subgrafos
  2. Eliminar los nodos que sus dos hijos sean isomorfos.



Un DDB se encuentra reducido a DDBR (Diagrama de decisión binario reducido ordenado) si tiene las siguientes características:
  • Unicidad: No existan dos nodos con el mismo símbolo proposicional ni con los mismos hijos izquierdo y derecho (nodos duplicados)
  • No redundancia: No existan nodos variables idénticos.



Con esto se redujo el primer árbol que observamos en la imagen. :)

lunes, 27 de agosto de 2012

Aplicación de la lógica proposicional

Lógica es el estudio del razonamiento, se refiere específicamente a si el razonamiento es correcto. 

Una proposición es un enunciado que puede afirmarse como verdadero o falso. 

"Lógica proposicional es la parte de la lógica que estudia la formación de proposiciones complejas a partir de proposiciones simples."


Proposiciones

Simples. Son las oraciones que se forman sin usar enlaces.
  • La casa es roja
  • Carlos es estudiante
Complejas. Son las oraciones que están formadas por dos o más proposiciones simples ligadas por un conector.
  • María es chef o es cantante
  • Si ayer llovió entonces hoy sale el sol
  • 2 es par y 9 es impar

Para validar preposiciones se necesita realizar las tablas de verdad, las cuales son diseños combinacionales dado por 2^n donde n es el número de proposiciones simples.

Los conectivos lógicos principales que son utilizados para formar proposiciones complejas son  ¬, ∨, ∧, →, ↔ ( no, o, y, si... entonces, si y sólo si ).

Las tablas de verdad de los conectivos principales son:


Conjunción.
La proposición p ^ q es verdadera solamente si p y q son verdaderas, en los demás casos es falsa.

Ejemplo:
Puedes salir cuando laves la ropa y arregles tu cuarto.



Disyunción.
La disyunción es verdadera si por lo menos una de las proposiciones es verdadera, y es falsa solamente cuando todas las preposiciones son falsas.

Por ejemplo.
Puedes ir a dormir o puedes hacer tu tarea



Implicación. 
La proposición p → q es falsa solamente si el antecedente es verdadero y el consecuente es falso. En los demás casos es verdadera.

Ejemplo.
p = Tengo dinero
q = Voy al cine
p → q = Si tengo dinero, entonces voy al cine

Doble implicación.
La proposición p ↔ q es verdadera cuando ambas preposiciones son verdaderas o ambas falsas.

Ejemplo.
r = El polígono es de cuatro lados
s = Es un cuadrilátero
r ↔ s = El polígono es de cuatro lados si y sólo si es un cuadrilátero.




Negación.
La negación es el conectivo lógico que permite cambiar el valor de verdad de una proposición.

Si p es verdadero, su negación ¬ es falsa y viseversa.

Por ejemplo. 
p = todos los triángulos son equiláteros
¬p = NO todos los triángulos son equiláteros



La lógica computacional puede ser aplicada al campo de la computación, su uso principal es en circuitos computacionales, programación lógica y análisis y optimización de algoritmos.

Sistema combinacional

Un sistema combinacional es un sistema digital en el que las salidas dependen de la combinación de sus entradas. Las funciones (OR, AND, NAND, XOR) son booleanas, o sea que cada función se puede representar en una tabla de verdad. 

Metodología de un sistema combinacional.

1. Especificar el sistema. En esta parte se detalla el propósito del diseño.

2. Determinar las entradas y salidas. Identificar las variables del problema, identificar entradas y salidas.

3. Construir la tabla de verdad. Trasladar el comportamiento del sistema a una tabla de verdad, indicando para cada combinación de entrada, la salida o salidas más convenientes para el diseño.

4. Minimizar. Para obtener las ecuaciones mínimas se pueden utilizar diferentes métodos como manipulación algebraica, mapas de karnaugh, entre otros.

5. Diagrama esquemático. Al obtener las ecuaciones mínimas, se representan en forma de símbolos para su análisis y comprensión.

6. Implementar. Hay dos formas de implementación, circuitos integrados de función fija (TTL) o dispositivos lógicos programables (PDLs).


Aplicación 

Para la tarea de esta semana nos pidieron lo siguiente:
"Investiguen aplicaciones de la lógica proposicional y documenten uno en su tercera tarea."

Para esta tarea explicaré una aplicación de circuitos combinatorios.

En una granja se tiene: 
  • Un granjero con una puerta muy grande y pesada en donde se requiere de varias personas para abrirla o cerrarla.
  • Un corral de ovejas.
  • Ocasionalmente llegan lobos.



El granjero necesita un sistema de alarma diseñado para lo siguiente:
  • Sea activado cuando las ovejas se encuentren fuera del corral y la puerta este abierta, para realizar una acción correctiva ya sea cerrar la puerta o poner las ovejas en el corral.
  • Sea activado cuando se encuentren los lobos cerca y las ovejas se encuentren fuera del corral, para realizar la acción correctiva de ahuyentar a los lobos.

1. Especificar el sistema
Las variables que intervienen son puerta, ovejas, lobos y alarma. Para las primeras tres variables se tienen sensores de deteccion.

Puerta
Abierta = 1 
Cerrada = 0

Ovejas
Fuera del corral = 1
Dentro del corral = 0

Lobos
Están cerca = 1 
Están lejos = 0

Para el dispositivo de alarma

Alarma
Activada = 1
Desactivada = 0


2. Determinar entradas y salidas
La puerta, las ovejas y los lobos (P, O y L) son las entradas del sistema, mientras que la Alarma (A) es la salida.

Diagrama de bloques.
3. Tabla de verdad

La alarma se activará cuando:
  • Las ovejas estén afuera y los lobos estén cerca.
  • La puerta esté abierta y las ovejas estén afuera del corral.
  • La puerta esté abierta, las ovejas estén afuera y los lobos estén cerca.


4. Minimizar

Para simplificar las ecuaciones utilizamos el método de Mapas de Karnaugh.


La ecuación quedaría de la siguiente manera:
F(A) = PO + OL 
F(A) = O (P + L)

Con esto se puede concluir que la alarma se activará cuando la puerta este abierta y las ovejas fuera del corral (PO) o cuando las ovejas estén fuera del corral y los lobos estén cerca (OL).


5. Diagrama esquemático



6. Implementación
La implementación se puede realizar con un dispositivo lógico programable (PLD) como el GAL16V8.

Referencias:
Proposiciones lógicas
Libro Matemáticas Discretas. Richard Johnsonbaugh. Sexta Edición.
Sistemas Digitales.