Resumen de LTS (Ingeniería I)

Labeled Transition System

Un LTS es un grafo compuesto por nodos y arcos etiquetados. Formalmente, es una tupla formada por S conjunto de nodos, A conjunto de aristas, $\Sigma$ alfabeto finito de etiquetas y $s_{k}$ estado inicial. Las transiciones se consideran no determinísticas.

Equivalencia

Hay distintas propuestas (todas fallidas) para determinar equivalencia:

• Idénticas (demasiado fuerte)
• Isomorfas (demasiado fuerte)
• Idénticas quitando estados no alcanzables (demasiado fuerte)
• Isomorfas quitando estados no alcanzables (demasiado fuerte)
• Igualdad de trazas (demasiado débil)

La equivalencia se define mediante la noción de bisimilaridad (fuerte o débil), la cual es una relación de equivalencia. Siendo P y Q estados de dos LTS distintas, dichas LTS son bisimilares sii para cada acción a:

• Cada vez que se ejecuta una acción a de un nodo P a uno P', debe ser posible que se ejecute la misma acción entre Q y Q', y que P' y Q' mantengan esta propiedad.
• Idem a la inversa.

La diferencia de bisimilaridad fuerte con débil, es que la débil considera acciones no observables (denominadas tau), las cuales no son tenidas en cuenta para la equivalencia.

No bisimilaridad puede probarse mediante un juego: el atacante se mueve por una LTS intentando que el defensor no pueda imitar sus acciones. Las LTS entonces son bisimilares si el defensor tiene estrategia ganadora, si no, no lo son.

Finite State Machines

Son una extensión de LTS, agregan condiciones, variables y opcionalmente relojes al grafo. Permiten describir el cuándo además del cómo en la especificación del problema.

Definición

El estado de una FSM se define como un par (s,v) donde s es el nodo y v es el estado actual de las variables y el tiempo del sistema. Vale que $s\in S$, $v\in V$ y $Is[v]=true$. El sistema solo puede permanecer en un nodo mientras $Is[v]=true$, el cual puede falsearse al aumentar el valor de los relojes.

La arista se define como una quintupla $(s,l,\psi ,\alpha ,s')$, perteneciente al conjunto A, donde s es el nodo de origen, l la label asociada, s' el nodo destino, $\psi$ la restricción para atravesarla y $\alpha$ la acción realizada, que convierte el estado v en v' destino.

Formalmente, la FSM es un sistema de transición etiquetado $T=(Q,\rightarrow )$ con:

• Estados $Q={(s,v)|s\in S,Is[v]=true}$
• Relación de transición $\rightarrow \subseteq Q*{L\cup R+}*Q$

Donde las relaciones de transición se dividen en temporales e instantáneas.

Composición

Un grafo temporizado puede definirse como la 4-upla $G=(S,X,A,I)$, donde S son los nodos, X el alfabeto, A las aristas e I el estado inicial.

La composición paralela de G1 y G2 sincronizando las etiquetas de $L'\subseteq L$ es denominada $G1|[L']|G2$.

Sean G1= <S1, X1, A1, I1> y G2= <S2, X2, A2, I2> tales que la intersección entre los alfabetos sea no vacía. La composición paralela entre ellos resulta un grafo tal que:

• S está contenido en el producto cartesiano de S1 x S2.
• X es la unión de X1 y X2
• I, el estado inicial, es el estado que resulta de I1 x I2.
• A, conjunto de aristas, está formado por todas aquellas aristas $a=(s,l,\psi ,\alpha ,s')$ tal que
  • a pertenece a A1 o A2 y su label l no pertenece al conjunto de labels sincronizadas L´ o
  • a se forma a partir de a1 y a2 tal que tienen la misma label perteneciente a L´, los nodos de origen y destino resultan de la unión de los nodos correspondientes, la condición $\psi$ es la conjunción de ambas y la acción $\alpha$ es la unión

Redes de Petri

Una red de Petri es un grafo bipartito en el que hay nodos de places y transitions. Los arcos van de places a transitions, y de esas transitions a otros places. Los places de origen son el preset de una transición y los de destino el posset. Cada arco tiene asociado un peso determinado.

Cada place puede contener una cantidad entera mayor o igual a cero de tokens. Una determinada asignación de tokens se denomina marking. Para poder efectuar una transición es necesario que los tokens de su preset sean iguales o superen los pesos de los ejes. Al efectuarse, dichos tokens se consumen, y se agregan en el posset los tokens especificados por los pesos de los ejes. La ejecución de estas transiciones es no determinística.

Considerando que hay un marking inicial, es posible definir el conjunto de markings alcanzables. Se dice que una red es N-safe dado un marking inicial sii no es alcanzable ningún marking en el que haya más de N tokens en un mismo place. Si se cumple esta propiedad, entonces es convertible a una FSM y viceversa.

Los usos de una red de Petri son similares a los de una FSM, para indicar las transiciones del sistema y determinar el "cuándo".

Diagramas de actividad

Los DA presentan un flujo de actividades que responden a un evento. Cada actividad se muestra conectada a la actividad que le continúa mediante una flecha que indica la transición entre ambas. El uso normal de una acción es modelar un paso o un conjunto de pasos en la ejecución de un algoritmo (un procedimiento). Son un tipo especial de red de petri.

Permite expresar decisiones en el flujo de actividad, notándolo mediante un diamante e indicando las condiciones booleanas en cada eje. También permite realizar forks y joins en el diagrama.

Las acciones pueden ser organizadas en andariveles, los cuales se usan para organizar las responsabilidades de las actividades. Usualmente corresponden a unidades organizacionales dentro de un modelo de negocio (por ejemplo áreas de una empresa), auqnue también pueden corresponderse con los actores de los casos de uso. Contribuyen a la identificación de responsabilidades. Puede usarse clustering además de andariveles.

Conveniencia de Uso

La mayor conveniencia de los DA es contar con una representación temprana del proceso total. Conviene utilizarlos para representar actividades que requieran coordinación, paralelismo o dependencias entre sí. Otro uso apropiado es para reflejar las interacciones entre varios casos de uso.

También permiten complementar el modelo de Casos de Uso mostrando la secuencia de un caso de uso, reflejando las interacciones entre varios casos y modelando el comportamiento interno del sistema. Ayudan a contar con una representación gráfica de procesos complejos de describir en texto, y conviene utilizarlos para representar actividades que requieran coordinación, paralelismo, dependencias entre sí, o múltiples condiciones.

Puede usarse para describir:

• Un método
• Un caso de uso
• La interacción entre varios casos de uso
• Explotar un paso del curso normal de un caso de uso.
• Un proceso de negocio (Workflow)

Este tipo de diagrama no es adecuado en situaciones donde ocurren eventos asincrónicos. Se centran en el procesamiento interno del sistema para cumplir una funcionalidad.

Data Flow Diagram

A data flow diagram (DFD) is a graphical representation of the "flow" of data through an information system. A data flow diagram can also be used for the visualization of data processing (structured design). It is common practice for a designer to draw a context-level DFD first which shows the interaction between the system and outside entities. This context-level DFD is then "exploded" to show more detail of the system being modeled (from Wikipedia).

Es semiformal, operacional (abstrae control), gráfico, refutable (si describe actividad existente). Su scope son operaciones y dependencias funcionales. La descomposición Top-Down es criticable pues difiere exactitud y toma decisiones tempranas. El problema en general: poca información es deducible de manera concluyente.

Message Sequence Charts

Los MSC son una versión simplificada de los diagramas de secuencia de UML. Se basan en el pasaje de mensajes entre distintos componentes y definen un ordenamiento de eventos.

Cada MSC genera una serie de trazas del sistema, al definir un orden parcial entre los eventos. Notar que si el envío de mensajes es sincrónico, el orden parcial es entre los mensajes, mientras que si es asincrónico, el orden afecta a los eventos de envío y recepción.

High level vs Basic

Un basic MSC (bMSC) es un diagrama que comprende a un sólo componente o escenario particular de todo el sistema. Para generar el sistema completo y unir los bMSC, se utilizan los high-level MSC (hMSC), que consiste en un LTS que posee como nodos a los bMSC. De esta manera, se define un orden en el que se ejecutan los distintos escenarios.

El sistema completo está dado por la composición de los bMSC siguiendo el hMSC. El problema surge al considerar las transiciones del hMSC asincrónicas. Esto es, el orden parcial entre los eventos se da solamente para los eventos que afectan a un único componente. Por lo tanto, si se tiene un hMSC con una secuencia A->B->C de bMSCs, y los componentes que tratan B y C son distintos, entonces es posible ejecutar C antes que B, ya que no hay ningún componente de C que reciba un mensaje para indicarle el fin de B. O sea, un bMSC no espera el fin del otro para comenzar, sino que se hace a nivel componente.

Los hMSC tienen un poder de expresividad limitado: hay ciertos protocolos o lenguajes regulares que no pueden expresar, es imposible utilizarlos para temporal model checking.

Síntesis

Tanto un bMSC como un hMSC pueden convertirse a LTSs. El orden parcial de los eventos en un bMSC permite generar un LTS asociado donde los mensajes son labels, y el hMSC puede convertirse a un LTS donde los bMSC son las labels.

Al realizar la conversión de diagrama de transiciones a estados, se generan más trazas de las existentes en el MSC. Esto significa que no son equivalentes, sino que las trazas posibles del MSC están contenidas (o son iguales) a las del LTS.

Estas trazas se corresponden con los llamados implied scenarios, es decir, escenarios no considerados en los MSC originales pero que se producen al realizar la composición de ellos y se evidencian en el LTS. Se pueden obtener generando la LTS correspondiente al hMSC y la LTS correspondiente a la composición de los componentes, utilizando los bMSC como labels. Así ambas LTS tienen el mismo alfabeto y se pueden detectar trazas de una que no pertenezcan a la otra.

En otras palabras, los métodos de detección se basan en construir modelos locales, componerlos y detectar trazas que no están incluidas en un modelo global de la especificación.

Estos escenarios implicados, no necesariamente malos, aparecen en cualquier implementación realizada del sistema que respete los MSC originales. Es necesario ampliarlos para evitar estas trazas. Los escenarios implicados revelan escenarios perdidos o una arquitectura incorrecta o demasiado abstracta.

An important observation on implied scenarios is that they are the result of an inconsistency between system decomposition and system behaviour. Implied scenarios are not an artefact of a particular MSC language, they are the result of specifying the global behaviours of a system that will be implemented component-wise.

Enlaces externos

• Jiri Srba: A Note on Game Characterizations of Strong and Weak Bisimilarity; Department of Computer Science, Aalborg University, Denmark.
• Anna Ingólfsdóttir: Lectures on Modelling, Specification and Verification; 12th Estonian Winter School in Computer Science.
• Sebastian Uchitel, Jeff Kramer and Jeff Magee: Detecting Implied Scenarios in Message Sequence Chart Specifications; Department of Computing, Imperial College, London.