Story Transcript
Escenarios Condicionales Existenciales: Sem´ antica y S´ıntesis
Diciembre de 2007
Tesista: German Emir Sibay Director: Dr. Sebastian Uchitel
Resumen Las especificaciones basadas en escenarios son una forma popular para describir el comportamiento del sistema a construir. Los modelos de comportamiento facilitan el an´alisis de dicho sistema y son tambi´en la base de t´ecnicas autom´aticas para hacerlo como model-checking, animaci´on y simulaci´on. Este trabajo se centra en facilitar el an´alisis temprano del comportamiento del sistema y el desarrollo de modelos de comportamiento junto con los escenarios. Se propone un nuevo lenguaje de especificaci´on basado en escenarios con una sem´antica existencial que permite especificaci´on condicional de comportamiento en forma de prechart y mainchart. La sem´antica del lenguaje es consistente con especificaciones de escenarios (informales) existentes y casos de uso. Este lenguaje es un mejor complemento para los Live Sequence Chart (LSC) universales que los LSC existenciales actuales que no expresan correctamente escenarios condicionales. La correspondencia entre el lenguaje propuesto y el LSC universal apunta a proveer un framework com´ un para, a partir de ejemplos, lograr descripciones completas a trav´es del proceso de relevamiento de requerimientos. Tambi´en se define un algoritmo de s´ıntesis que construye modelos de comportamiento en la forma de Modal Transitions System (MTS). Los MTSs distinguen entre comportamiento posible, requerido y prohibido. Al refinarlo se garantiza la preservaci´on de los escenarios y adem´as permite el relevamiento de requerimientos.
3
Agradecimientos Esta tesis es el resultado de un a˜ no de trabajo durante el cual aprend´ı mucho m´as que los resultados aqu´ı provistos. Fundamentalmente a investigar. Hace ya casi 4 a˜ nos comenc´e a trabajar en la industria del software alej´andome de manera progresiva de la Universidad. Sent´ı la necesidad de volver e intentar el camino de la ciencia. Vi´endolo en retrospectiva estoy convencido de haber tomado una excelente decisi´on. Sin embargo no tengo m´as que palabras de agradecimiento para con mis compa˜ neros de trabajo de Hexacta con quienes, a´ un habi´endome alejado de la empresa, sigo teniendo un contacto fluido. Tengo que agradecer enormemente a Sebasti´an Uchitel por haber cre´ıdo en mi al darme un tema de investigaci´on tan importante y haberme guiado durante mi transici´on industria-ciencia (¡y continuar haci´endolo!). No puedo dejar de mencionar al resto de mis compa˜ neros del grupo de investigaci´on LAFHIS: Victor Braberman, Diego Garbervetsky, Fernando Schapachnik, Fernando Asteasuain, Guido de Caso, Nicol´as D´Ippolito, Esteban Pavese y Mat´ıas Lorger. Me hicieron sentir como en casa, realmente un placer trabajar con todos ellos. Agradezco de coraz´on a todos los que conforman la Universidad de Buenos Aires y muy especialmente a los docentes que he tenido, desde los profesores titulares hasta los ayudantes ad honorem. Gracias a todos ellos es que me siento orgulloso de pertenecer a esta instituci´on. Mucho fue lo que aprend´ı de mis eternos compa˜ neros de TP: Diego Figueira, Daniel Jercog, Mart´ın Rouaux y Mat´ıas Tencer. Sobre todo, como trabajar y divertirse al mismo tiempo. A mi familia le agradezco el haberme apoyado siempre a´ un sin entender un pomo lo que hac´ıa (ni siquiera el nombre de la carrera que estudi´e). A mi viejo por evitar que mi peso baje a niveles alarmantes atiborr´andome de asado y vino. A mi vieja por haberme mostrado los libros de chiquito y a mi hermana por ense˜ narme el lado top de la vida. No puedo olvidarme de mis t´ıos y primos que me tuvieron que aguantar de chiquito, gracias. 5
6 Fundamentalmente tengo que agradecerle a la Biblioteca del C´ırculo Popular de Cultura de Z´arate porque fue ah´ı, entre sus anaqueles, donde realmente me form´e entre los 7 y 10 a˜ nos de edad. A mis amigos de Z´arate por haberme acompa˜ nado en la escuela de la calle. No los voy a nombrar por temor (y seguridad) de olvidarme alguno. Y tambi´en a los personajes Zaratokas, desde la vieja Zanahoria hasta los pileteros del N´autico (por ejemplo el que te ense˜ naba a patear la pelota porque dec´ıa que hab´ıa jugado en River). Podr´ıa tener una vida feliz sin todo lo que aprend´ı luego, no sin lo que aprend´ı en Z´arate. Finalmente le agradezco profundamente a mi novia, Yanina. Los momentos culminantes de la tesis fueron tan estresantes para ella como para m´ı. Gracias por haberme aguantado, haberme ayudado en mi hogar y por quererme a pesar de haberme vuelto, lentamente, un poco (solo un poco) nerd.
´Indice general
1. Introducci´ on
15
2. Conocimientos previos
19
2.1. S´ımbolos, palabras y lenguajes . . . . . . . . . . . . . . . . . . . .
19
2.2. Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
20
2.2.1. Sistema de transici´on etiquetada (LTS) . . . . . . . . . . .
21
2.2.2. Sistema modal de transici´on etiquetada (MTS) . . . . . . .
22
2.3. Escenarios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
29
2.3.1. Diagrama de secuencia . . . . . . . . . . . . . . . . . . . .
29
2.3.2. Live Sequence Charts - eLSC y uLSC . . . . . . . . . . . .
32
3. Nueva modalidad de LSC
35
3.1. Live Sequence Chart: existencial, universal . . . . . . . . . . . . .
35
3.2. LSC existencial con Prechart (epLSC)
. . . . . . . . . . . . . . .
36
3.3. Sem´antica sobre un ´arbol de ejecuciones . . . . . . . . . . . . . .
38
´ 3.3.1. Arbol de ejecuciones . . . . . . . . . . . . . . . . . . . . .
38
3.3.2. Satisfacci´on de epLSC por un ´arbol de ejecuciones . . . . .
39
´ 3.3.3. Arbol de ejecuciones de un LTS . . . . . . . . . . . . . . .
40
7
´INDICE GENERAL
8 4. S´ıntesis
43
4.1. S´ıntesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
43
4.1.1. Introducci´on . . . . . . . . . . . . . . . . . . . . . . . . . .
43
4.1.2. Algoritmo . . . . . . . . . . . . . . . . . . . . . . . . . . .
48
4.1.3. Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . .
52
5. Correcci´ on del algoritmo de s´ıntesis
57
5.1. Resultados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
57
5.2. Demostraci´on de correcci´on . . . . . . . . . . . . . . . . . . . . .
59
6. Completitud del algoritmo de s´ıntesis
61
6.1. Resultados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
61
6.2. Demostraci´on de completitud . . . . . . . . . . . . . . . . . . . .
62
6.2.1. Definici´on de relaci´on de refinamiento d´ebil . . . . . . . . .
62
6.2.2. Demostraci´on de relaci´on de refinamiento d´ebil . . . . . . .
65
7. Caso de estudio
69
7.1. Mine Pump . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
69
7.2. Metodolog´ıa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
69
7.3. Iteraciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
70
8. Conclusiones
79
8.1. Contribuciones . . . . . . . . . . . . . . . . . . . . . . . . . . . .
79
8.2. Trabajos relacionados . . . . . . . . . . . . . . . . . . . . . . . . .
80
8.3. Trabajo futuro
82
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
´INDICE GENERAL
9
Appendices
83
A. Demostraciones
85
A.1. Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
85
A.1.1. Demostraci´on Teorema 1 . . . . . . . . . . . . . . . . . . .
85
A.2. Correcci´on . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
86
A.2.1. Lemas . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
86
A.2.2. Demostraci´on Teorema 2 . . . . . . . . . . . . . . . . . . .
87
A.2.3. Demostraci´on Teorema 4 . . . . . . . . . . . . . . . . . . .
88
A.2.4. Demostraci´on Teorema 6 . . . . . . . . . . . . . . . . . . .
89
A.3. Completitud . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
89
A.3.1. Demostraci´on Teorema 10 . . . . . . . . . . . . . . . . . .
89
B. Caso de estudio
91
Bibliograf´ıa
99
10
´INDICE GENERAL
´Indice de figuras
2.1. Un LTS simple que modela una m´aquina expendedora de bebidas
21
2.2. Un MTS simple que modela una m´aquina expendedora de bebidas
22
2.3. MTS modalando un lock de lectura, con una transici´on τ representando un c´omputo interno . . . . . . . . . . . . . . . . . . . .
24
2.4. MTS modalando un lock de lectura . . . . . . . . . . . . . . . . .
25
2.5. M´aquina de Bebidas de la Figura 2.1 habiendo ocultado noSugar
25
2.6. Reglas para el operador Hiding . . . . . . . . . . . . . . . . . . .
26
2.7. Sem´antica del operador satisface . . . . . . . . . . . . . . . . . . .
27
2.8. Un MSC de un ATM . . . . . . . . . . . . . . . . . . . . . . . . .
29
2.9. Un MSC de una m´aquina expendedora de caf´e. Tiene una co-regi´on. 30 2.10. Un Live Sequence Chart existencial (eLSC) . . . . . . . . . . . . .
32
2.11. Un Live Sequence Chart universal(uLSC) . . . . . . . . . . . . . .
33
3.1. Un LSC existencial con Prechart (epLSC) . . . . . . . . . . . . .
38
3.2. un LTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
40
3.3. Arbol de ejecuciones del LTS de la Figura 3.2 . . . . . . . . . . .
41
3.4.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
41
3.5.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
11
12
´INDICE DE FIGURAS 4.1. Un epLSC de un ATM . . . . . . . . . . . . . . . . . . . . . . . .
43
4.2. MTS sintetizado a partir del epLSC en la Figura 4.1 . . . . . . . .
44
4.3. Una implementaci´on no determin´ıstica del MTS de la Figura 4.2 .
45
4.4. El LTS de la Figura 4.3 con su alfabeto restringido al del epLSC de la Figura 4.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . .
46
4.5. Una implementaci´on determin´ıstica del MTS de la Figura 4.2 . . .
47
4.6. El LTS de la Figura 4.5 con su alfabeto restringido al del epLSC de la Figura 4.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . .
47
4.7. MTS sintetizado a partir del escenario de la Figura 3.4 . . . . . .
53
4.8. MTS sintetizado a partir del escenario de la Figura 3.5 . . . . . .
53
4.9. Escenario con una co-regi´on . . . . . . . . . . . . . . . . . . . . .
54
4.10. MTS sintetizado a partir del escenario de la Figura 4.9 . . . . . .
54
4.11. Escenario con un Prechart y Mainchart que se solapan . . . . . .
55
4.12. MTS sintetizado a partir del escenario de la Figura 4.11 . . . . . .
55
6.1. LTS X . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
64
6.2. LTS Y . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
64
7.1. Escenario 1 del Mine Pump . . . . . . . . . . . . . . . . . . . . .
71
7.2. Escenario 2 del Mine Pump . . . . . . . . . . . . . . . . . . . . .
71
7.3. MTS sintetizado a partir del escenario de la Figura 7.2 . . . . . .
72
7.4. Fluents y acciones iniciales para el caso de estudio . . . . . . . . .
73
7.5. Propiedades iniciales para el caso de estudio . . . . . . . . . . . .
73
7.6. LTSs del ambiente y el aparato bomba . . . . . . . . . . . . . . .
74
7.7. Propiedades φ1 y φ2 relajadas . . . . . . . . . . . . . . . . . . . .
75
7.8. Escenario 3 del Mine Pump . . . . . . . . . . . . . . . . . . . . .
76
´INDICE DE FIGURAS
13
7.9. MTS sintetizado a partir del escenario de la Figura 7.8 . . . . . .
77
7.10. Propiedades φ3 y φ4
77
. . . . . . . . . . . . . . . . . . . . . . . . .
14
´INDICE DE FIGURAS
Cap´ıtulo 1 Introducci´ on “He perdido la cifra de los a˜ nos que yazgo en la tiniebla; yo, que alguna vez era joven y pod´ıa caminar por esta prisi´on, no hago otra cosa que aguardar, en la postura de mi muerte, el fin que me destinan los dioses. Con el hondo cuchillo de pedernal he abierto el pecho de las v´ıctimas, y ahora no podr´ıa, sin magia, levantarme del polvo.” La escritura del dios - Jorge Luis Borges
Los modelos de comportamiento operacionales como los Labelled Transitions Systems (LTSs) [1] son formalismos u ´ tiles y convenientes para modelar y razonar acerca del comportamiento de los sistemas a un nivel arquitect´onico. Describen al sistema como un conjunto de componentes que interact´ uan, donde cada componente es modelado como una m´aquina de estados, y la interaccion entre los componentes sucede a trav´es de eventos compartidos. Estos modelos son la base para un amplio espectro de t´ecnicas autom´aticas de an´alisis, como model-checking y simulaci´on. Una de las mayores limitaciones del modelado y an´alisis es la complejidad de la construcci´on de dichos modelos. La construcci´on de modelos contin´ ua siendo una tarea dif´ıcil, larga y reservada a expertos. Para paliar esto se han investigado y desarrollado un amplio espectro de t´ecnicas para la s´ıntesis autom´atica (o semiautom´atica) de modelos de comportamiento. Por ejemplo, a partir de escenarios y casos de uso (e.g., [2, 3, 4, 5, 6]), se ha estudiado extensamente. Especificaciones basadas en escenarios como Message Sequence Charts (MSCs) [7] describen la forma en que los componentes del sistema, el ambiente, y los usuarios interactuan a fin de proveer la funcionalidad del sistema. Su simplicidad y representaci´on gr´afica intuitiva facilita la participaci´on de los stakeholders 15
16
´ CAP´ITULO 1. INTRODUCCION
y los hace populares para el relevamiento de requerimientos. La s´ıntesis desde especificaciones basadas en escenarios ayuda al an´alisis temprano, validaci´on y refinamiento incremental de modelos de comportamiento. Una amplia variedad de lenguajes de escenarios y t´ecnicas de s´ıntesis asociadas a ellos se han desarrollado y usado en numerosos casos de estudios. Estos lenguajes incluyen construcciones para describir alternativas y comportamiento repetitivo (ciclos), instancias simb´olicas, informaci´on de estados. Tambi´en se han estudiado extensiones que permiten expresar expl´ıcitamente causalidad a trav´es de condiciones y triggers (gatillos). Es interesante la variaci´on sem´antica en cuanto a la interpretaci´on existencial o universal de los distintos enfoques. Un escenario existencial da un ejemplo del comportamiento del sistema, comportamiento que el sistema tiene que proveer. Un escenario universal provee una regla que todo el comportamiento del sistema debe satisfacer. Mientras que t´ıpicamente cada enfoque est´a basado en una interpretaci´on o la otra, existe un lenguaje llamado Live Sequence Chart (LSC) [4] que provee construcciones sint´acticas y soporte sem´antico para ambas interpretaciones. La motivaci´on para dicho lenguaje es que durante el proceso de relevamiento de requerimientos hay una transici´on progresiva desde declaraciones existenciales, en forma de ejemplos y casos de uso, hacia afirmaciones universales, en la forma de propiedades. Entonces un lenguaje basado en escenarios que soporte ambas interpretaciones est´a mejor equipado para proveer esta transici´on. Pese a la variedad de enfoques que existen en la actualidad, no hay un lenguaje (y algoritmo de s´ıntesis asociado) adecuado para describir escenarios existenciales condicionales. Por ejemplo consideremos la declaraci´on “si el usuario inserta una tarjeta v´alida en el ATM, y luego ingresa la clave correcta, el/ella puede solicitar efectivo y obtenerlo del ATM”. Esta afirmaci´on, probablemente provista como un caso de uso, es existencial en el sentido que provee un ejemplo de ejecuci´on del sistema. Tambi´en es condicional en el sentido que solicitar y obtener efectivo se espera que sea posible si el usuario ha insertado una tarjeta v´alida e ingresado la clave correcta. Algunos enfoques [4, 2, 8] proveen construcciones sint´acticas para describir relaciones condicionales o causales entre secuencias de acciones (eventos). Sin embargo, todos ellos tienen una interpretaci´on universal. Por ejemplo, los LSCs universales (uLSCs) que describen comportamiento condicional a trav´es de un prechart y un mainchart se interpret´an as´ı: una vez que sucede el prechart, el mainchart debe suceder. Esta sem´antica es apropiada para describir afirmaciones como “cuando el usuario ingresa incorrectamente la clave tres veces seguidas, el
17 ATM debe retener su tarjeta”. Los escenarios condicionales con sem´antica existencial se ajustan naturalmente a los enfoques basados en casos de uso. Los casos de uso t´ıpicamente se interpretan de manera existencial y contienen precondiciones, por ejemplo casos de uso para retirar efectivo, cambiar la clave e imprimir un balance de cuentas podr´ıan tener la misma precondici´on. Estos casos de uso no son mutuamente excluyentes y se espera que el sistema pueda proveer al menos esa funcionalidad cuando la precondici´on se satisfaga. Adem´as, esta sem´antica se ajusta bien con m´etodos de relevamiento (e.g. [9]) que utilizan preguntas “que tal si” en forma de secuencia de interacciones y relevan algunas de las respuestas del sistema. Cada respuesta puede ser codificada con escenarios condicionales existenciales, en contraposici´on con escenarios condicionales universales, ya que probablemente es desconocido si la respuesta del sistema corresponde a una respuesta obligatoria o simplemente posible del sistema. En esta tesis se define un nuevo lenguaje de especificaci´ on de escenarios que permite describir escenarios condicionales existenciales en el sentido explicado anteriormente. Los escenarios contienen un prechart y un mainchart con el mismo estilo que los uLSCs, pero se interpretan existencialmente: cuando sucede el prechart, el sistema debe poder realizar el mainchart. Llamaremos a este nuevo tipo de escenario Live Sequence Chart existencial con prechart (epLSC) para distinguirlo del escenario existencial provisto en LSC que no soporta de manera adecuada la descripci´on de comportamiento existencial condicional. La complementaci´on entre epLSC y uLSC es un avance en el objetivo de proveer un framework uniforme para trasladarnos desde ejemplos hacia descripciones completas a trav´es del proceso de relevamiento de requerimientos. En este trabajo tambi´en se define un algoritmo de s´ıntesis a un modelo de comportamiento a partir de epLSCs. El algoritmo construye un sistema de transici´on modal (MTS) [10]. Este modelo es una m´aquina de estados que puede distinguir entre comportamiento requerido, posible y prohibido del sistema a ser construido. El MTS sintetizado a partir del epLSC caracteriza, a trav´es de una noci´on formal de refinamiento, a todas las implementaciones que satisfacen el epLSC. Los MTS son modelos parciales y sus implementaciones son LTSs (sistemas de transici´on etiquetados). Entonces el MTS sintetizado caracteriza a todos los LTSs que satisfacen el escenario. Sintetizar de una manera compacta una representaci´on de todos los posibles LTS que satisfacen una descripci´on dada por un epLSC tiene varias ventajas. Por un lado se evita seleccionar arbitrariamente un LTS espec´ıfico cuando hay varios
18
´ CAP´ITULO 1. INTRODUCCION
que satisfacen. Adem´as, un MTS se puede utilizar para an´alisis y exploraci´on de diferentes alternativas de implementaciones a partir de un epLSC. Tambi´en se puede refinar iterativamente a medida que se releva nueva informaci´on. Estos refinamientos efectivamente reducen el conjunto de LTSs descriptos por el MTS y son una caracterizaci´on m´as precisa y completa del comportamiento del sistema a construir. Este refinamiento iterativo puede ser alimentado por t´ecnicas tradicionales de an´alisis como inspecci´on, animaci´on y model checking. Adem´as, el refinamiento puede producirse a trav´es de merges [11] del MTS con otros MTSs resultado de la s´ıntesis [12] de otros escenarios (sean epLSCs u otros) y/o especificaciones declarativas. El resto de esta tesis se organiza de la siguiente manera. En el Cap´ıtulo 2 se detallan los formalismos existentes utilizados en este trabajo. En el Cap´ıtulo 3 se discute sobre los lenguajes basados en escenarios y se presenta el nuevo lenguaje condicional existencial. En el Cap´ıtulo 4 hay un algoritmo de s´ıntesis a MTS a partir de un epLSC y en los Cap´ıtulos 5 y 6 se dan la demostraciones de correcci´on y completitud del algoritmo de s´ıntesis. El uso de los epLSC se realiza en un caso de estudio en el Cap´ıtulo 7. Finalmente en el Cap´ıtulo 8 se discute el trabajo en general, se lo compara con otros y se presentan las conclusiones.
Cap´ıtulo 2 Conocimientos previos “...quise recordar, en mi sombra, todo lo que sab´ıa. Noches enteras malgast´e en recordar el orden y el n´ umero de unas sierpes de piedra o la forma de un ´arbol medicinal. As´ı fui revelando los a˜ nos, as´ı fui entrando en posesi´on de lo que ya era m´ıo.” La escritura del dios - Jorge Luis Borges
2.1.
S´ımbolos, palabras y lenguajes
A continuaci´on se presentan conceptos de lenguajes utilizados durante toda esta tesis. Un lenguaje es simplemente un conjunto de palabras. Una palabra es una secuencia de s´ımbolos de alg´ un alfabeto. Finalmente un alfabeto es un conjunto de s´ımbolos. Notaci´ on. Σ es un conjunto de s´ımbolos y ǫ es la cadena vac´ıa. Dado un conjunto + K, K es la clausura transitiva de K y K ∗ la clausura reflexiva transitiva de K. Las partes de K se nota ℘(K). Proyectar una palabra w ∈ Σ∗ sobre un alfabeto A ⊆ Σ, notado w|A es descartar de w los s´ımbolos que no est´ an en A. Formalmente es la palabra que se obtiene aplicando la regla recursiva: ǫ|A = ǫ y, para e ∈ A, ue|A = u|A e y, para e ∈ / A ue|A = u|A . Se define prefijos de una palabra: Definici´ on 1 (prefijos de una palabra). pref ijos : Σ∗ → ℘(Σ∗ ) pref ijos(α) = { β ∈ Σ∗ | ∃γ ∈ Σ∗ βγ = α } 19
CAP´ITULO 2. CONOCIMIENTOS PREVIOS
20
Esta definici´on se extiende a conjunto de palabras o lenguaje: Definici´ on 2 (prefijos de un conjunto de palabras o lenguaje). pref ijos : ℘(Σ∗ ) → ℘(Σ∗ ) pref ijos(L) = { β ∈ pref ijos(γ) | γ ∈ L } De una manera similar se define sufijos: Definici´ on 3 (sufijos de una palabra). suf ijos : Σ∗ → ℘(Σ∗ ) suf ijos(α) = { β ∈ Σ∗ | ∃γ ∈ Σ∗ γβ = α } De manera an´aloga que para prefijos se extiende la definici´on de sufijos a conjunto de palabras o lenguajes Definici´ on 4 (sufijos de un conjunto de palabras o lenguaje). suf ijos : ℘(Σ∗ ) → ℘(Σ∗ ) suf ijos(L) = { β ∈ suf ijos(γ) | γ ∈ L } Para un conjunto de palabras definimos firsts como el conjunto de s´ımbolos que cumplen ser primer s´ımbolo de alguna de dichas palabras. Definici´ on 5 (firsts). f irsts : ℘(Σ∗ ) → ℘(Σ) f irsts(R) = { a | aα ∈ R } follows del s´ımbolo t y el conjunto R son las palabras w tal que tw est´a en R. Definici´ on 6 (follows). f ollows : ℘(Σ∗ ) × Σ → ℘(Σ∗ ) f ollows(R, t) = { α | tα ∈ R }
2.2.
Modelos
En esta secci´on se presentan los modelos de comportamientos que se utilizar´an en esta tesis y se fija la notaci´on. Primero se presentan los LTS, modelos de transici´on etiquetados utilizados ampliamente para el modelado y an´alisis de sistemas concurrentes y distribuidos. Luego se introducen los MTS que son sistemas de transici´on modales que no est´an completamente definidos y de esta manera representan un conjunto de LTSs (sus implementaciones). Finalmente se introducen algunas operaciones sobre estos modelos como refinamiento, hiding (ocultamiento) y merge.
2.2. MODELOS
2.2.1.
21
Sistema de transici´ on etiquetada (LTS)
Un LTS [1] es un sistema de transici´on de estados donde las transiciones est´an etiquetadas con acciones. El conjunto de acciones de un LTS se llama alfabeto de comunicaci´on y constituye las interacciones que el sistema modelado puede tener con el ambiente. Adem´as un LTS puede tener transiciones etiquetadas con τ , representando transiciones que no son observables por el ambiente.
Figura 2.1: Un LTS simple que modela una m´aquina expendedora de bebidas
Un ejemplo de un LTS puede verse en la Figura 2.1. Por convenci´on se etiqueta con 0 el estado inicial. El resto de los n´ umeros de estados est´an solo como referencia y carecen de sem´antica. Las transiciones con varias acciones es una forma resumida de indicar una transici´on individual por cada una de las acciones. Definici´ on 7 (Sistema de transici´on etiquetado). Sea States el conjunto universal de estados, Act el conjunto universal de etiquetas de acciones observables, y sea Actτ = Act ∪ { τ }. Un sistema de transici´on etiquetado (LTS, labelled transition system) es una tupla P = (S, L, ∆, s0 ), donde S ⊆ States es un conjunto finito de estados, L ⊆ Actτ es un conjunto de etiquetas, ∆ ⊆ (S × L × S) es una relaci´on de transici´on entre estados, y s0 ∈ S es el estado inicial. Se usa αP = L \ {τ } para notar el alfabeto de comunicaci´ on de P . Notaci´ on. Dado un LTS P = (S, L, ∆, s0 ) decimos que P transita por ℓ a P ′ , ℓ notado P −→ P ′, si P ′ = (S, L, ∆, s′0 ) y (s0 , ℓ, s′0 ) ∈ ∆. ǫ τ ℓ τ ℓ τ P =⇒ P ′ denota P (−→)∗ P ′ . Se usa P =⇒ P ′ para notar P (−→)∗ −→ (−→)∗ P ′ . Para ℓ ∈ Actτ , ℓˆ = ℓ si ℓ 6= τ y ℓˆ = ǫ si ℓ = τ . w Sea w = w1 , . . . , wk una palabra sobre Actτ . Entonces P −→ P ′ significa que wi+1 existen P0 , . . . , Pk tal que P = P0 , P ′ = Pk , y Pi −→ Pi+1 para 0 ≤ i < k. Se w w escribe P −→ para decir ∃P ′ · P −→ P ′. Finalmente, se extiende =⇒ a palabras de igual manera que se hizo para −→.
22
2.2.2.
CAP´ITULO 2. CONOCIMIENTOS PREVIOS
Sistema modal de transici´ on etiquetada (MTS)
Un sistema modal de transici´on etiquetada (MTS) [10] permite el modelado expl´ıcito de lo que no se conoce sobre el comportamiento del sistema. Extienden los LTS con un conjunto de transiciones que modelan interacciones con el ambiente que el sistema no puede garantizar proveer pero tampoco puede garantizar prohibir. Definici´ on 8 (Sistema modal de transici´on etiquetado). Un sistema modal de transici´on etiquetado (MTS, modal transition system) M es una tupla (S, L, ∆r , ∆p , s0 ), donde ∆r ⊆ ∆p , (S, L, ∆r , s0 ) es un LTS representando transiciones requeridas del sistema y (S, L, ∆p , s0 ) es un LTS representando posibles (pero no necesariamente requeridas) transiciones del sistema. Se nota con αM = L al alfabeto de comunicaci´ on de M.
Figura 2.2: Un MTS simple que modela una m´aquina expendedora de bebidas Un ejemplo de un MTS se ve en la Figura 2.2. Hay una transici´on maybe desde y hacia el estado 0 con el r´otulo noSugar. Un LTS que resulta ser implementaci´on (la definici´on formal de implementaci´on se da m´as adelante) es el de la Figura 2.1. Otra implementaci´on posible es un LTS que tenga como requerida la transici´on noSugar. Este MTS est´a modelando una m´aquina expendedora de bebidas, pero al momento de modelar se est´an aceptando implementaciones que permitan seleccionar bebidas sin agregado de az´ ucar, y tambi´en implementaciones donde no existe la posibilidad de elegir (no existe dicha transici´on). Notaci´ on. El conjunto de todos los MTS es δ. Dado un MTS M = (S, L, ∆r , ∆p , s0 ) w y sea w = w1 , . . . , wk una palabra sobre Actτ . Entonces M −→r M ′ significa que
2.2. MODELOS
23 wi+1
existen M0 , . . . , Mk tal que M = M0 , M ′ = Mk , y Mi −→r Mi+1 para 0 ≤ i < k. w w Se escribe M −→r para decir ∃M ′ · M −→r M ′ . Para γ ∈ {p, r}, se escribe ǫ τ M =⇒γ M ′ para denotar M(−→γ )∗ M ′ . Para ℓ 6= τ y γ ∈ {p, r} se escribe ℓ τ ℓ τ M =⇒γ M ′ para denotar M(−→γ )∗ −→γ (−→γ )∗ M ′ . Para γ ∈ {p, r} se extiende =⇒γ a palabras de manera an´aloga a −→γ . Para γ ∈ {p, r} y ℓ ∈ Actτ , a veces ℓ ℓ escribimos s −→γ s′ para decir Ms −→γ Ms′ ′ donde Ms es el MTS M con el estado inicial cambiado a s. Las transiciones con la flecha fina se conocen como transiciones simples y las transiciones con flecha doble son transiciones observables. Todo LTS (S, A, ∆, s0 ) puede verse como un MTS de la siguiente forma (S, A, ∆, ∆, s0 ), es decir, un MTS con todas sus transiciones requeridas. En esta tesis asumimos que todos los MTS (y por ende los LTS) son de trazas infinitas: Definici´ on 9 (Trazas infinitas). Un MTS M = (S, L, ∆r , ∆p , s0 ) es de trazas a infinitas si para todo s ∈ S, existe un a ∈ Actτ y s′ ∈ S tal que Ms −→p Ms′ Es decir que un MTS es de trazas infinitas si cada estado tiene al menos una transici´on saliente.
Refinamiento Refinamiento de un MTS captura la noci´on de ir puliendo el modelo a medida que se gana conocimiento sobre el comportamiento que hab´ıa sido modelado con transiciones maybe. Al refinar un modelo se pasa a uno m´as completo. Es una relaci´on “m´as definido que” entre dos modelos parciales. Intuitivamente, refinar un MTS es convertir transiciones maybe en requeridas o removerlas. Un MTS N refina M si N preserva todo el comportamiento requerido y prohibido de M. Dicho de otra forma, un MTS N refina M si N puede simular el comportamiento requerido de M, y M puede simular el comportamiento posible de N. El refinamiento d´ebil u observacional [13] permite comparar el comportamiento observable entre modelos, ignorando las posibles diferencias que puedan tener en t´erminos de c´alculos o computaciones internas. Estas computaciones no son observables por el ambiente y se modelan con transiciones τ .
CAP´ITULO 2. CONOCIMIENTOS PREVIOS
24
Durante esta tesis, siempre que se hable de refinamiento, se hace referencia a Refinamiento observacional: Definici´ on 10 (Refinamiento observacional). N es un refinamiento observacional de M, notado M N, si αM = αN y (M, N) est´ a contenido en alguna relaci´on de refinamiento R ⊆ δ × δ para la cual vale que para todo ℓ ∈ Actτ : ℓ
ℓˆ
ℓ
ℓˆ
1. (M −→r M ′ ) =⇒ (∃N ′ · N =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R) 2. (N −→p N ′ ) =⇒ (∃M ′ · M =⇒p M ′ ∧ (M ′ , N ′ ) ∈ R) Por ejemplo sea N el MTS de la Figura 2.3 y M el de la Figura 2.4, N es refinamiento de M(M N) a trav´es de la relaci´on de refinamiento R = { (M0 , N0 ), (M1 , N1 ), (M1 , N2 ) }. El modelo m´as refinado tiene un c´omputo interno antes de liberar el lock.
Figura 2.3: MTS modalando un lock de lectura, con una transici´on τ representando un c´omputo interno La definici´on de refinamiento observacional est´a basada en la de bisimulaci´on d´ebil. La definici´on considera de a un paso de la simulaci´on, pero puede extenderse a una traza. Cada vez que se transita un camino en una m´aquina, tiene que existir un camino en la otra pero sin tener en cuenta las transiciones τ . El siguiente teorema nos permite considerar trazas en lugar de una sola transici´on: Teorema 1. Sean M, N ∈ δ (de trazas infinitas) tal que M N donde R ⊆ δ ×δ es la relaci´on de refinamiento y αM = αN = Σ. Para cuaquier β ∈ (Σ ∪ { τ })+ : β
β|Σ
M −→r M ′ =⇒ (∃N ′ · N =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R) β
β|Σ
N −→p N ′ =⇒ (∃M ′ · M =⇒p M ′ ∧ (M ′ , N ′ ) ∈ R) Demostraci´on. Ver Ap´endice A.1.1
2.2. MODELOS
25
Figura 2.4: MTS modalando un lock de lectura Un MTS puede tener transiciones que representan c´omputo interno o simplemente no deber´ıan ser observables por el ambiente. Pueden ocultarse con el operador de hiding. Definici´ on 11 (Hiding). Sea M un MTS (S, L, ∆r , ∆p , s0 ) y Z ⊆ Act un conjunto de acciones observables. M con las acciones de Z ocultas, notado M \ Z ′ ′ ′ ′ es un MTS (S, L \ Z, ∆r , ∆p , s0 ) donde ∆r y ∆p son las relaciones m´ as chicas que satisfacen las reglas en la Figura 2.6 tal que γ ∈ {r, m}. Usamos M@Z para decir M \ (Act \ Z). El MTS de la Figura 2.2, al ocultar (aplicar el operador de hiding) noSugar, se obtiene el de la Figura 2.5. El LTS (visto como MTS) de la Figura 2.1 es un refinamiento del de la Figura 2.5. Los LTSs que refinan un MTS M son
Figura 2.5: M´aquina de Bebidas de la Figura 2.1 habiendo ocultado noSugar descripciones completas del comportamiento del sistema en cuanto al alfabeto de M. Dichos LTSs son implementaciones de M. Un MTS puede pensarse como
26
CAP´ITULO 2. CONOCIMIENTOS PREVIOS
Figura 2.6: Reglas para el operador Hiding un modelo que representa al conjunto LTSs que lo implementan. La diversidad del conjunto resulta de tomar diferentes decisiones en cuanto al comportamiento posible (maybe) del MTS. Definici´ on 12. (Implementaci´on) Se dice que un LTS I = (SI , A, ∆I , i0 ) es una implementaci´on de un MTS M = (SM , A, ∆rM , ∆pM , m0 ), notado M I, si M MI donde MI = (SI , A, ∆I , ∆I , i0 ). Notaci´ on. Se nota al conjunto de implementaciones de un MTS M como I[M] = { I LT S | M I }.
El refinamiento preserva implementaciones. Esto significa que si un MTS es refinado, el conjunto de implementaciones que caracteriza se reduce. Formalmente, si M M ′ entonces I[M] ⊇ I[M ′ ]. Hacer merge de MTSs [11] es el proceso de combinar lo que se sabe de cada descripci´on parcial, es decir, es la construcci´on de un MTS que incluya todo el comportamiento requerido y que prohiba todo el prohibido de cada MTS, y es lo menos refinado posible. Formalmente, merge de MTSs es el proceso de encontrar su refinamiento com´ un m´ınimo. Definici´ on 13 (Refinamiento com´ un m´ınimo). Sean Q, M, y N MTSs. Q es un refinamiento com´ un (CR) de M y N si αQ = (αM ∪ αN), M@αQ Q y N@αQ Q. Q es un refinamiento com´ un m´ınimo (MCR) de M y N si Q es ′ un CR de M y N y no hay un MTS Q 6≡ Q tal que Q′ es un CR de M y N, y Q′ Q.
Dados dos MTS M y N, un MCR para ellos puede no existir, en cuyo caso se dice que M y N son inconsistentes, o puede que no sea u ´ nico [11]. En [14], se provee un algoritmo que construye un CR a partir de MTSs consistentes. Se ha demostrado que este algoritmo produce un MCR en el caso que M y N tengan el mismo alfabeto, pero una prueba de que tambi´en lo hace cuando hay alfabetos distintos a´ un no ha sido provista.
2.2. MODELOS
27
π |= Fl , π 0 |= Fl π |= Xφ , π 1 |= φ
π |= ¬φ , ¬(π |= φ) π |= Gφ , ∀i ≥ 0 · π i |= φ
π |= φ ∧ ψ , (π |= φ) ∧ (π |= ψ)
Figura 2.7: Sem´antica del operador satisface Fluents y FLTL Los fluents se utilizan para razonar acerca de los efectos de acciones sobre estados de un sistema. Definici´ on 14. Un fluent Fl se define por un par de conjuntos IFl , el conjunto de acciones iniciadoras, y TFl , el conjunto de acciones finalizadoras: Fl = hIFl , TFl i donde IFl , TFl ⊆ Act y IFl ∩ TFl = ∅. Un fluent puede ser inicialmente true o false indicado por el atributo Initially Fl y se asume false si no se incluye el atributo. Cada acci´on a ∈ Act induce un fluent; a saber: a = ha, Act \ {a}i. FLTL [15] es una l´ogica para razonar sobre fluents. Definici´ on 15. Dado el conjunto de fluents Φ, Fl ∈ Φ es una f´ ormula FLTL, y otras f´ormulas FLTL se definen inductivamente usando los conectivos booleanos conocidos y los operadores temporales X (next), U (strong until), W (weak until), F (eventually), and G (always). Notaci´ on. Sea Π el conjunto de trazas infinitas sobre Act. Para π = a0 , a1 , . . . ∈ Π, se nota π i al sufijo de π comenzando en ai . Definici´ on 16. π = a0 , a1 , . . . satisface un fluent Fl, notado π |= Fl, si y solo si vale alguna de las siguientes condiciones: • •
InitiallyFl ∧ (∀j ∈ N · 0 ≤ j ≤ i ⇒ aj ∈ / TFl ) ∃j ∈ N · (j ≤ i ∧ aj ∈ If ) ∧ (∀k ∈ N · j < k ≤ i ⇒ ak ∈ / TFl )
En otras palabras, un fluent vale en un cierto momento si y solo si vale inicialmente, u ocurri´o alguna acci´on iniciadora, y en ambos casos, no ha sucedido una acci´on finalizadora. La Figura 2.7 muestra el operador de satisfacci´on |= para algunos operadores de FLTL [15]. La sem´antica trivaluada de FLTL sobre un MTS M da el valor de cada f´ormula φ ∈ FLTL en M. La sem´antica se da en funci´on de las trazas de un MTS. Definici´ on 17 (Trazas de un MTS). Sea M un MTS, una traza π = a0 , a1 , . . . , donde ai ∈ Act es una traza true en M si hay una secuencia infinita {Mi } tal
CAP´ITULO 2. CONOCIMIENTOS PREVIOS
28 a
i que M0 = M y Mi =⇒ r Mi+1 para todo i ∈ N. Una traza π es una traza maybe en M si no es una traza true , pero existe una ai secuencia infinita {Mi } tal que M0 = M y Mi =⇒ p Mi+1 para todo i ∈ N. Una traza π es una traza possible en M si es una maybe o true . Finalmente, una traza π es una traza false en M si no es una traza possible.
Notaci´ on. Se nota el conjunto de trazas true , maybe , possible, y false sobre un MTS M como TrueTr(M), MaybeTr(M), PosTr(M) y FalseTr(M) respectivamente.
Entonces, en base a las trazas del MTS se define cuando una f´ormula FLTL satisface al modelo. Definici´ on 18. Sea φ una f´ormula FLTL y M un MTS, φ es true en M (notado M |= φ) si cada traza en PosTr(M) satisface φ, y false en M (notado M 6|= φ) si hay una traza en TrueTr(M) que refuta φ, o si cada traza en PosTr(M) refuta φ. Sino, φ evalua como maybe en M.
La propiedad m´as importante es que el refinamiento preserva las propiedades true y false : Propiedad 1. (Preservaci´on de FLTL) Sea M un MTS. Entonces ∀φ ∈ FLTL, M |= φ =⇒ ∀I ∈ I[M] · I |= φ y M 6|= φ =⇒ ∀I ∈ I[M] · I 6|= φ
Entonces, si una propiedad se eval´ ua como true en M, es true en todas las implementaciones de M, y si una propiedad se eval´ ua como false en M, es false en todas sus implementaciones. En [16], se detalla un procedimiento M(x) para construir autom´aticamente un MTS a partir de propiedades FLTL de safety (i.e. a formulas que pueden siempre ser refutadas de manera finita). Este procedimiento asegura que M(φ) caracteriza a todos los modelos LTS que satisfacen la propiedad φ. Propiedad 2 (Caracterizaci´on de φ [16]). Si φ es una propiedad de safety satisfacible, entonces para toda implementaci´ on LTS de trazas infinitas L, L |= φ ⇔ L ∈ I[M(φ)].
2.3. ESCENARIOS
2.3. 2.3.1.
29
Escenarios Diagrama de secuencia
Los diagramas de secuencia son el nucleo de un conjunto de notaciones ampliamente aceptadas para la descripci´on de escenarios, como Message Sequence Charts (MSC) [7] y Diagramas de Interacci´on de UML. La sint´axis b´asica, puede verse en la Figura 2.8, consta de l´ıneas verticales llamadas lifelines que representan instancias de alg´ un componente involucrado en la interacci´on descripta. Los diagramas de secuencia denotan interacci´on entre instancias a trav´es de flechas. Estas interacciones, llamadas mensajes, pueden representar comunicaci´on sincr´onica o asincr´onica entre las instancias. En el caso de la primera, el mensaje representa un evento instant´aneo con el cual ambas instancias sincronizan. En el segundo, el mensaje representa dos eventos instantaneos: uno asociado al origen de la flecha, el env´ıo del mensaje, y otro asociado con el destino de la flecha. En esta tesis se asume que los mensajes son sicr´onicos, por simplicidad. Si se consideran asincr´onicos, el lenguaje que genera un diagrama se define de otra manera (la secuencia de interacci´on es distinta), pero todos los resultados de esta tesis siguen valiendo.
Figura 2.8: Un MSC de un ATM Los diagramas de secuencia se leen de arriba hacia abajo, el tiempo se asume que corre en esa direcci´on. Un diagrama de secuencia define un orden parcial de eventos basado en la regla: un evento en una lifeline puede ocurrir si todos los eventos m´as arriba en la misma lifeline han ocurrido.
30
CAP´ITULO 2. CONOCIMIENTOS PREVIOS
Tambi´en pueden definirse regiones que contienen eventos para denotar que no hay un ´orden entre ellos. Se las llama co-regiones [7]. Gr´aficamente se notan con una l´ınea punteada entre eventos a la derecha del diagrama. Por ejemplo en la Figura 2.9 hay una co-regi´on definida entre los eventos coin y pressButton. Es decir, no importa en que orden pasen estos eventos. Pero si es importante que solo cuando han sucedido estos dos eventos sucede cof ee (se entrega el caf´e).
Figura 2.9: Un MSC de una m´aquina expendedora de caf´e. Tiene una co-regi´on. Representaci´ on abstracta y sem´ antica Los escenarios se representan abstractamente como ordenes parciales etiquetado (Labeled Partial Order, LPO). Esta es la forma est´andar de dar sem´antica a los MSC o Diagramas de Interacci´on de UML 2.0. Definici´ on 19 (Order Parcial A-Etiquetado (A-LPO)). Un Order Parcial AEtiquetado (A-LPO) es una tupla hL, ≤, λ, Ai donde L es un conjunto finito de locaciones ≤⊆ L × L es una relaci´ on de orden parcial sobre L. Es entonces reflexiva (l ≤ l), anti sim´etrica (l ≤ l′ , l′ ≤ l implica l = l′ ) y transitiva (l ≤ l′ , l′ ≤ l′′ implica l ≤ l′′ ). λ : L → A es una funci´on que aplica etiquetas. El comportamiento del sistema se da a trav´es de sus ejecuciones, es decir, sus secuencias de eventos. Hay que relacionar LPOs con secuencias de eventos. Esto se hace a trav´es del concepto de linearizacion. Intuitivamente, la relaci´on temporal/causal de los diagramas de secuencia puede ser asociada con ejecuciones de un LPO. En particular, si un LPO impone que l ≤ l′ , entonces l siempre debe suceder antes que l′ en cualquier ejecuci´on.
2.3. ESCENARIOS
31
Definici´ on 20 (Linearizaci´on). Una linearizaci´ on de un A-LPO hL, ≤, λ, Ai es ∗ una palabra u = e0 . . . en ∈ A tal que el LPO hLu , ≤u , λu , Ai es isomorfo a hL, ≤′ , λ, Ai con ≤⊆≤′ , donde las locaciones son los ´ındices de u Lu = { 0, . . . , n } el orden total es el orden de los naturales i ≤u j ⇐⇒ i ≤ j para 0 ≤ i, j ≤ n La funci´on de etiquetado mapea cada ´ındice con el s´ımbolo de u en esa posici´on, λu (i) = ei Dicho de otra manera, una palabra u es una linearizaci´on del A-LPO G si hay una secuencia de locaciones l0 . . . ln tal que: a) las etiquetas de las locaciones concuerdan con u (λ(l0 ) . . . λ(ln ) = u) y b) el orden parcial descripto por G es respetado en la secuencia. Entonces se define el lenguage de un A-LPO G como el conjunto de sus linearizaciones. Definici´ on 21 (Lenguaje de un A-LPO). Se nota al lenguaje un A-LPO G = hL, ≤, λ, Ai como: LG = { u ∈ A∗ | u es una linearizaci´ on de G } Se introdujeron los LPOs para tener un objeto simple que describa la informaci´on contenida en un diagrama de secuencia (MSC o Diagramas de interacci´on). Esta es su sintaxis abstracta. La sem´antica de estos diagramas puede darse en t´erminos de los LPOs. Sin embargo, hay que explicar como se pasa de un diagrama concreto a un LPO. El mecanismo est´a descripto en [7]. Un mensajes se denota con una flecha que apunta a la instancia receptora o a la misma instancia si es un mensaje local. Los puntos del diagrama en los cuales los eventos (mensajes) ocurren ser´an llamados en esta secci´on puntos. Un LPO se obtiene a partir de un diagrama siguiendo estas reglas. Una locaci´on en el LPO es un conjunto de puntos de la forma { p } si es un evento local en p o { p, q } si hay una flecha de p a q. La etiqueta de la locaci´on ser´a simplemente el nombre del evento realizado en su(s) punto(s). Por definici´on, los puntos de una misma locaci´on concuerdan en su etiqueta (evento). Queda definir como se ordenan las locaciones. Dos locaciones est´an directamente ordenadas (l1 donde α ∈ pref ijos(LP ) y Θ ∈ ℘(suf ijos(LM )) es un conjunto de sufijos de palabras en el lenguaje del Mainchart. La primer componente del estado (α en el ejemplo anterior) ser´a sufijo de cualquier ejecuci´on que lleve a s (y adem´as est´a en LP ). Se utiliza para llevar cuenta de que porci´on del Prechart se ha avistado y de esa manera detectar cuando se cumple (el Prechart). De hecho α = suf ijoSignif icativo(π) (Definici´on 28) donde π es una ejecuci´on que lleva a s. Resulta ser el sufijo m´as largo de una ejecuci´on que es prefijo del Prechart (prefijo de una palabra de LP ). El conjunto de palabras Θ ∈ ℘(suf ijos(LM )) representa las obligaciones restantes generadas por las ejecuciones que llevan a s. Es decir son los sufijos de palabras del Mainchart que tienen que suceder para que la activaci´on del Prechart en la ejecuci´on que llev´o a s se satisfaga. Caminos requeridos por las obligaciones tienen que existir a partir de s para satisfacer el epLSC. Definici´ on 28 (sufijoSignificativo). suf ijoSignif icativo : (ΣR ∪ { τ })∗ → pref ijos(LP ) suf ijoSignif icativo(π) = m´ax|β| { β | π = zβ ′ ∧ β ′ |ΣR = β ∧ β ∈ pref ijos(LP ) } Dada un estado s =< α, Θ >, la palabra α describe la porci´on del Prechart que ha sido cubierto por la ejecuci´on que llev´o al estado s; intuitivamente es lo que nos interesa de las ejecuciones que llevaron a ese estado. Por simplicidad, se habla de un sufijo significativo en vez de decir el sufijo significativo de una ejecuci´on finita (lo cual ser´ıa lo correcto). Para conocer, dado un sufijo significativo y una transici´on en ΣR ∪ { τ } o una secuencia de transiciones ((ΣR ∪ { τ })∗ ) cual es el sufijo significativo del estado al cual se llega usaremos la siguiente funci´on: Definici´ on 29 (next). next : pref ijos(LP ) × (ΣR ∪ { τ })∗ → pref ijos(LP ) next(α, ǫ) = α next(α, tβ) = next(suf ijoSignif icativo(αt), β) t ∈ ΣR ∪ { τ }
4.1. S´INTESIS
49
Propiedad 3. Sea α un sufijo significativo suf ijoSignif icativo(α) = α Demostraci´on. Directo de la definici´on de sufijo significativo. Definici´ on 30 (newObligations). newObligations : (ΣR ( ∪ { τ })∗ → suf ijos(LM ) LM suf ijoSignif icativo(α) ∩ LP 6= ∅ newObligations(α) = ∅ sino Algoritmo El algoritmo de s´ıntesis (ver Algoritmo 1) comienza con un MTS sin transiciones y un estado inicial (l´ıneas 3-9). El estado inicial del MTS es < ǫ, ∅ >, es decir el estado donde no se ha reconocido ning´ un prefijo del Prechart del epLSC y no se han contra´ıdo obligaciones. El algoritmo toma cada estado s =< α, Θ > sin marcar del MTS (l´ınea 11), lo marca y luego, para cada etiqueta en el scope, agrega transiciones y, quiz´as, nuevos estados alcanzados por dichas transiciones (l´ınea 14). Adem´as, si en el estado hay obligaciones se agrega una transici´on τ cuya finalidad es ir a un estado que olvide las obligaciones heredadas de estados anteriores. Sin embargo en el siguiente estado (luego de transitar por τ ) el valor de newObligations(α) = newObligations(ατ ), con lo cual las nuevas obligaciones surgidas al valer el Prechart en el estado siguen estando. Es correcto que estas obligaciones no puedan ser olvidadas ya que si en un estado vale el Prechart, al transitar por τ tambi´en vale. El criterio para agregar transiciones y estados se basa en los valores de α y Θ. Se encuentra encapsulado en el procedimiento addT ransitions. El algoritmo termina cuando todos los estados agregados por el procedimiento addT ransitions han sido marcados. El n´ ucleo del algoritmo est´a en el procedimiento addT ransitions. El procedimiento agrega al menos una transici´on por t a partir de s =< α, Θ >. Puede ser que agregue varias transiciones requeridas por t para satisfacer cada una de las obligaciones en Θ que comienzan con ese s´ımbolo. Primero se computa la porci´on del Prechart que se detecta una vez que t ocurre (l´ınea 3). Luego se calcula el conjunto de obligaciones para los estados alcanzados tomando la transici´on t desde s. Las obligaciones pueden surgir de dos formas: nuevas y heredada.
CAP´ITULO 4. S´INTESIS
50
1 3 4 5 6 7 9 11 12 14 15 16 17
Data: E = ⋄(P, M, ΣR ) Result: W = (S, ΣR , ∆r , ∆p , s0 ) tal que W I ⇔ I |= E. begin ∆r ←− ∅; ∆p ←− ∅; s0 ←−< ǫ, ∅ >; S ←− ∅; W ←− (S, Σ, ∆r , ∆p , s0 ); add(s0 ,S); while unmarked(S) 6= ∅ do < α, Θ > ←− get(unmarked(S)); mark(< α, Θ >); foreach t ∈ ΣR do addTransitions(S, < α, Θ >, t, ∆r , ∆p ) if Θ 6= ∅ then /* obligations exists for this state */
18
20 21 22
/* add a τ transition that forgets them */ addTransitions(S, < α, Θ >, τ, ∆r , ∆p ) return W ; end Algorithm 1: S´ıntesis de MTS
4.1. S´INTESIS
1
3
5
7 8 10
12 13
14 15
17 19 20 21
23 24
26 27 28 29
begin /* get significant suffix for next state */ α′ ←− next(α, t); /* get obligations for next state */ if sufijos(α′ ) ∩ LP 6= ∅ then /* prechart holds */ newObligations ←− LM ; else newObligations ←− ∅; /* no new obligations */ /* add transitions */ /* add new required branch for each obligation starting with t */ foreach θ′ ∈ follows(Θ, t ) do if θ′ = ǫ then /* t ends with obligation */ inheritedObligation ←− ∅; else /* propagate old obligation without initial t */ inheritedObligation ←− { θ′ }; nextState ←− < α′ , inheritedObligation ∪ newObligations >; add(( < α, Θ >, t , nextState), ∆p ); add(( < α, Θ >, t , nextState), ∆r ); /* Add new state if not previously visited */ addIfNotPresent(nextState, S); if t ∈ / firsts(Θ) then /* add maybe transition */ nextState ←−< α′ , newObligations >; add(( < α, Θ >, t ,nextState), ∆p ); addIfNotPresent(nextState, S); end Procedure addTransitions(S,< α, Θ >, t, ∆r , ∆p )
51
CAP´ITULO 4. S´INTESIS
52
Las nuevas corresponden a newObligations(αt). Entonces, si al suceder t se completa el Prechart (l´ınea 5), entonces todas las palabras del Mainchart se transforman en nuevas obligaciones (l´ınea 7). Caso contrario no hay nuevas obligaciones (l´ınea 10). Luego el procedimiento agrega las transiciones. Las transiciones se agregan de distinta manera seg´ un si hay o no obligaciones comenzando con t (a fin de agregar a los estados destino una obligaci´on heredada si existiese). Si hay obligaciones comenzando con t, tienen que agregarse transiciones de tal manera que se cumplan. Se hace agregando transiciones no determin´ısticas requeridas t. Esta eleccion no determin´ıstica representa las ramas en las cuales el MTS debe asegurar la existencia de una ejecuci´on donde est´en presentes las obligaciones adquiridas por haberse cumplido el Prechart (l´ıneas 12-23). Si no es el final de la obligaci´on se pone lo que resta de la obligaci´on en el conjunto inheritedObligation (l´ınea 17). Caso contrario inheritedObligation es el conjunto vac´ıo. Luego las obligaciones del siguiente estado ser´an las nuevas obligaciones productos de la u ´ ltima transici´on (LM o ∅, dependiendo de si vale o no el Prechart) y lo que resta de la obligaci´on que se est´a transitando (l´ınea 19). Si no hay obligaciones que comienzan por t, entonces t ∈ / f irsts(Θ). Con lo cual se agrega la transici´on maybe por t (l´ınea 26). Vale notar que en el caso en que t es τ entonces f ollows(Θ, τ ) = ∅ y τ ∈ / f irsts(Θ), lo que significa que no hay obligaciones por τ . Esto hace que las transiciones τ sean siempre maybe. Adem´as next(α, τ ) = α con lo cual si en un estado α vale el Prechart, el estado al cual se llega transitando por τ , tambi´en vale el Prechart y tiene todo LM entre sus obligaciones.
4.1.3.
Ejemplos
En las Figuras 4.7 y 4.8 est´a el resultado de sintetizar los escenarios de las Figuras 3.4 y 3.5 respectivamente. El escenario de la Figura 4.9 define un Mainchart con dos palabras. El MTS sintetizado por el algoritmo est´a en la Figura 4.10 Finalmente en el escenario de la Figura 4.11 hay un solapamiento entre Prechart y Mainchart. El Prechart se satisface tambi´en en el Mainchart. El MTS sintetizado por el algoritmo est´a en la Figura 4.12
4.1. S´INTESIS
Figura 4.7: MTS sintetizado a partir del escenario de la Figura 3.4
Figura 4.8: MTS sintetizado a partir del escenario de la Figura 3.5
53
54
CAP´ITULO 4. S´INTESIS
Figura 4.9: Escenario con una co-regi´on
Figura 4.10: MTS sintetizado a partir del escenario de la Figura 4.9
4.1. S´INTESIS
Figura 4.11: Escenario con un Prechart y Mainchart que se solapan
Figura 4.12: MTS sintetizado a partir del escenario de la Figura 4.11
55
56
CAP´ITULO 4. S´INTESIS
Cap´ıtulo 5 Correcci´ on del algoritmo de s´ıntesis “En la otra celda hab´ıa un jaguar; en su vecindad percib´ı una confirmaci´on de mi conjetura y un secreto favor.” La escritura del dios - Jorge Luis Borges
5.1.
Resultados
Siendo W el MTS resultante de aplicar el Algoritmo 1 sobre un escenario sc, hay que demostrar que toda implementaci´on de W satisface sc. La demostraci´on ser´a por reductio ad absurdum. Suponiendo que existe una implementaci´on de W que no satisface, entonces tiene que existir una ejecuci´on finita donde vale el Prechart, pero tal que alguna palabra del Mainchart no es la proyecci´on de ninguna posible continuaci´on de la ejecuci´on. Esta suposici´on llevar´a a una contradicci´on. Antes de la demostraci´on, algunos resultados intermedios. Teorema 2. Sea α un sufijo significativo, γ, β ∈ (ΣR ∪ { τ })∗ next(α, γβ) = suf ijoSignif icativo(next(α, γ)β) Demostraci´on. Ver Ap´endice A.2.2 Corolario 3. Sea α un sufijo significativo, β ∈ (ΣR ∪ { τ })∗ next(α, β) = suf ijoSignif icativo(αβ) 57
58
´ DEL ALGORITMO DE S´INTESIS CAP´ITULO 5. CORRECCION
Demostraci´on. Directo del teorema anterior tomando γ = ǫ y usando next(α, ǫ) = α. Con estos resultados puede demostrarse que siendo W el MTS resultante del Algorimto 1, desde cualquier estado, al transitar una ejecuci´on cuya proyecci´on en ΣR est´a en LP , el estado al que se llega tiene entre sus obligaciones todo LM Teorema 4 (Si vale el Prechart, alg´ un sufijo del sufijo significativo del estado pertenece al Prechart). Sea W = (S, Σ, ∆r , ∆p , s0 ) el MTS resultante del Algoritmo 1 y < α, Θ >∈ S ∀β ∈ (ΣR ∪ { τ })∗ · β|ΣR ∈ LP =⇒ β
∀ < α′ , Θ′ >∈ S · (< α, Θ >−→< α′ , Θ′ > =⇒ suf ijos(α′) ∩ LP 6= ∅)
Es decir, para cualquier β ∈ (ΣR ∪ { τ })∗ tal que su proyecci´ on est´ a en LP vale que alg´ un sufijo del sufijo significativo del estado al que se llega transitando por β a partir de < α, Θ > est´a en LP . Demostraci´on. Ver ap´endice A.2.3 Corolario 5 (Si vale el Prechart, el Mainchart est´a incluido en obligaciones). Sea W = (S, Σ, ∆r , ∆p , s0 ) el MTS resultante del Algoritmo 1 y < α, Θ >∈ S ∀β ∈ (ΣR ∪ { τ })∗ · β|ΣR ∈ LP =⇒ β
∀ < α′, Θ′ >∈ S · (< α, Θ >−→< α′ , Θ′ > =⇒ LM ⊆ Θ′ )
Es decir, para cualquier β ∈ (ΣR ∪ { τ })∗ tal que su proyecci´ on est´ a en LP vale que LM est´a incluido en las obligaciones del estado al que se llega transitando por β a partir de < α, Θ >. Demostraci´on. Si suf ijos(α′) ∩ LP 6= ∅ el algoritmo agrega en las obligaciones del estado con ese sufijo significativo (en este caso < α′ , Θ′ >) todo LM . Es decir LM ⊆ Θ′ . Teorema 6. Sea W = (S, Σ, ∆r , ∆p , s0 ) el MTS resultante del Algoritmo 1 y < α, Θ >∈ S, θ ∈ Θ ∀β ∈ ΣR · θ = βγ ∧ |β| > 0 =⇒ β
∃ < α′ , Θ′ >∈ S· < α, Θ >−→r < α′ , Θ′ > ∧ (γ = ǫ ∨ γ ∈ Θ′ )
Es decir, para cualquier obligaci´ on θ ∈ Θ y cualquier descomposici´ on βγ de θ, al transitar β, si β no es θ (es solo un prefijo propio), el estado al que se llega tiene como obligaci´on a γ.
´ DE CORRECCION ´ 5.2. DEMOSTRACION
59
Demostraci´on. Ver Ap´endice A.2.4 Corolario 7 (Por cada obligaci´on hay un camino requerido). Sea W = (S, Σ, ∆r , ∆p , s0 ) el MTS resultante del Algoritmo 1 y < α, Θ >∈ S θ
∀θ ∈ suf ijos(LM ) · θ ∈ Θ =⇒ < α, Θ >−→r Demostraci´on. Si θ ∈ Θ entonces |θ| > 0. Si considero β = θ es un caso particular del teorema anterior.
5.2.
Demostraci´ on de correcci´ on
Ahora si estamos en condiciones de demostrar que toda implementaci´on del W del Algoritmo 1 satisface el escenario a partir del cual fue creado. Para ello usaremos algunos de los resultados anteriores. Teorema 8 (El algoritmo de s´ıntesis es correcto). El MTS resultado del Algoritmo 1 satisface el escenario que le dio origen. Formalmente: Sea sc un epLSC tal que sc = ♦(P, M, ΣR ) y sea W el resultado de aplicar el Algoritmo 1 a sc entonces ∀X@ΣR ∈ I[W ] =⇒ X |= sc Demostraci´on. Sea W el resultado del Algoritmo 1 supongamos que existe un LTS X de trazas infinitas tal que X@ΣR es refinamiento de W pero no satisface el escenario sc (es decir X 6|= sc). Si X 6|= sc entonces X@ΣR 6|= sc ya que solo importa, para ver si se satisface o no un cierto escenario, el scope de sc (Definiciones 25 y 27). Como X@ΣR no satisface el escenario tiene que existir una ejecuci´on finita Π = α′ β ′ α′ β ′ con α′ , β ′ ∈ (ΣR ∪ { τ })∗ tal que siendo β = β ′ |ΣR y X@ΣR −→ X ′ :
γ′
β ∈ LP ∧ ∃γ ∈ LM · ∄γ ′ ∈ (ΣR ∪ { τ })∗ · γ = γ ′ |ΣR ∧ X ′ −→
(5.1)
X@ΣR se puede ver como un MTS con todas sus transiciones requeridas. En α′ β ′ particular son transiciones posibles con lo cual X@ΣR −→p X ′ . Entonces ,por α′ β ′ |Σ
teorema 1, hay un W ′′ tal que W =⇒R p W ′′ . α′ |Σ
β ′ ΣR
Sea W =⇒R p W ′ =⇒ p W ′′ y como β ′|ΣR = β y β ∈ LP entonces, por el Corolario 5, LM est´a en las obligaciones de W ′′ .
´ DEL ALGORITMO DE S´INTESIS CAP´ITULO 5. CORRECCION
60
Entonces, seg´ un el corolario 7, para cada obligaci´on en W ′′ hay un camino requerido. Es decir γ
∀γ ∈ LM · W ′′ −→r entonces por Teorema 1 y sabiendo que γ|ΣR = γ γ
∀γ ∈ LM · X ′ =⇒r Esto u ´ ltimo significa que para cada palabra de LM se puede transitar desde ′ X , posiblemente tomando algunas transiciones τ en el camino. Formalmente significa que para todo γ ∈ LM hay un γ ′ ∈ (ΣR ∪ { τ })∗ con γ ′ |ΣR = γ tal que γ′
X ′ −→r . Esto contradice la ecuaci´on 5.1. El absurdo vino de suponer que existe una implementaci´on de W (de trazas infinitas) que no satisface el escenario.
Cap´ıtulo 6 Completitud del algoritmo de s´ıntesis “Consider´e que en el lenguaje de un dios toda palabra enunciar´ıa esa infinita concatenaci´on de los hechos, y no de un modo impl´ıcito, sino expl´ıcito, y no de un modo progresivo, sino inmediato. Con el tiempo, la noci´on de una sentencia divina pareci´ome pueril o blasfematoria. Un dios, reflexion´e, s´olo debe decir una palabra, y en esa palabra la plenitud.” La escritura del dios - Jorge Luis Borges
Esta secci´on se centra en la demostraci´on de la completitud del Algoritmo 1. Esto quiere decir que dado W resultado del algoritmo a partir de un escenario sc, todo LTS X que satisface sc cumple W X@ΣR . Antes algunos resultados u ´ tiles.
6.1.
Resultados
Cuando se hable de un MTS con todas sus transiciones requeridas (una implementaci´on) se usar´a indistintamente =⇒r y =⇒. Teorema 9 (W es no bloqueante en ΣR ). Sea W = (S, Σ, ∆r , ∆p , s0 ) el MTS resultante del Algoritmo 1, s ∈ S: α
∀α ∈ Σ∗R · s =⇒p 61
CAP´ITULO 6. COMPLETITUD DEL ALGORITMO DE S´INTESIS
62
Demostraci´on. Para cada estado el algoritmo agrega transiciones para todo ΣR a trav´es del Procedimiento addTransitions. En el algoritmo se agrega para cada estado, al menos una transici´on por cada t ∈ ΣR .
6.2.
Demostraci´ on de completitud
Sea X un LTS que satisface un escenario sc con alfabeto ΣR y W el resultado del Algoritmo 1 con dicho escenario queremos ver que W X@ΣR . Si encontramos entre W y X@ΣR una relaci´on de refinamiento lo habremos logrado. Vamos a construir una relaci´on entre estos MTS (X@ΣR puede ser visto como un MTS con todas sus transiciones requeridas).
6.2.1.
Definici´ on de relaci´ on de refinamiento d´ ebil
La relaci´on se va a armar agregando para cada α ∈ (ΣR ∪ { τ })∗ y cada α X tal que X@ΣR =⇒ X ′ tuplas de relaci´on entre X ′ y los W ′ que cumplen ′
α|Σ
R ′ ′ W =⇒ a, por Corolario 3, p W (con lo cual el sufijo significativo de W0 ser´ suf ijoSignif icativo(α)). Si bien W es completo con respecto a ΣR , las transiciones τ cuando hay obligaciones, hacen que haya varios W ′ que cumplen lo anterior. La idea es elegir los W ′ de tal manera que sea una relaci´on de refinamiento.
Esta relaci´on es una especie de bisimulaci´on donde W simula el comportamiento posible de X@ΣR y X@ΣR simula el comportamiento requerido de W . Por ello al armar la relaci´on hay que tener la precauci´on de elegir los W ′ de tal manera de desviarnos de los caminos requeridos de W (surgidos por las obligaciones al valer el Prechart) siempre que el camino que se est´a simulando de X@ΣR no puede completar una palabra del Mainchart. Entonces, para cada palabra α que forma un camino a partir de X@ΣR , se van a relacionar los X ′ a los cuales se llega, con alg´ un W ′ donde el sufijo signi′ ficativo de W0 va a ser el de α y las obligaciones de W0′ tendr´an como obligaci´on heredada a lo que falta de la obligaci´on que puede completarse desde X ′ (si la hubiera) o no tendr´a obligaci´on heredada cuando desde X ′ no se pueda completar una obligaci´on surgida de haber valido el Prechart antes. En ambos casos W ′ tendr´a entre sus nuevas obligaciones LM si y solo si con α vale el Prechart. Entonces las obligaciones de W ′ son las nuevas (surgidas si vale el Prechart con α) y, si la hubiera, una heredada (la continuaci´on de una obligaci´on surgida de un Prechart anterior).
´ DE COMPLETITUD 6.2. DEMOSTRACION
63
Siempre puede encontrarse un W ′ que cumpla lo anterior ya que a partir que vale el Prechart se puede seguir los caminos requeridos por cada obligaci´on y en cualquier punto tomar una transici´on τ (el algoritmo agrega una transici´on τ a los estados de W que tienen alguna obligaci´on) que olvide la obligaci´on heredada si es que se quiere simular un X ′ que ya no puede continuar con ella. Notar que si vale el Prechart, por m´as que se tome una transici´on τ se va a un estado donde vale el Prechart y hay obligaciones. Sin embargo esta no es una obligaci´on heredada que pueda olvidarse sino que es una nueva obligaci´on surgida de la u ´ ltima transici´on y no estar´ıa bien no respetarlas ya que si en el estado actual vale el Prechart y tomamos una transici´on τ el Prechart sigue valiendo, por lo cual, debemos seguir teniendo en las obligaciones a todo LM . Entonces dependiendo de α, y de si el X ′ al que se llega permite completar una palabra del Mainchart surgida de una obligaci´on, se lo relaciona con los W ′ tales que su estado inicial tiene como sufijo significativo a suf ijoSignif icativo(α) y como obligaciones las nuevas producto de haber transitado por α y, si fuera posible, una obligaci´on heredada que pueda completarse desde X ′ Definici´ on 31 (RW,X@ΣR ). Sea sc un epLSC, W el resultado del Algoritmo 1 y X es un MTS con todas sus transiciones requeridas (es decir, una implementaci´ on) tal que X sc se define RW,X@ΣR como: RW,X@ΣR =
α
(W ′ , X ′) | α ∈ (ΣR ∪ { τ })∗ · X@ΣR =⇒ X ′ ∧
α|Σ
R ′ W =⇒ p W ∧ ( obligaciones(W0′ ) = newObligations(α) ∪ { θ } ∧ θ ∈ inheritedObligations(α, X ′ ) ) ∨ ( obligaciones(W0′ ) = newObligations(α) )
Las obligaciones heredadas inheritedObligations(α, X ′ )(Definici´on 32) son las obligaciones surgidas de un Prechart que vali´o antes de completar α y que pueden ser completadas desde X ′ (lo que resta de ellas). Por ejemplo, si tenemos un epLSC tal que LP = { k } y LM = { a b c, a b d } y el LTS X de la Figura 6.1 (notar que satisface el epLSC) vale: inheritedObligations(k, X1 ) = ∅ ya que no vali´o un Prechart antes de k (vale exactamente con k). inheritedObligations(ka, X2 ) = { b c, b d } ya que antes de ka se cumpli´o el Prechart (con k) y, luego de a falta completarse b c y b d de las obligaciones (es decir, son obligaciones heredadas) y ambas pueden ser completadas desde X2 . Por esto mismo vale inheritedObligations(kab, X3 ) = { c, d }. Si consideramos el mismo epLSC y el LTS Y de la Figura 6.1 (que satisface el epLSC) vale:
64
CAP´ITULO 6. COMPLETITUD DEL ALGORITMO DE S´INTESIS
Figura 6.1: LTS X
Figura 6.2: LTS Y
inheritedObligations(k, Y1 ) = ∅. inheritedObligations(ka, Y2 ) = { b c, b d }. Hasta ahora es igual a lo sucedido con X. Sin embargo, si bien desde Y2 pueden completarse las obligaciones heredadas b c y b d, lo hacen por caminos distintos. Desde Y3 se puede completar la obligaci´on heredada c y desde Y4 d. Por ello: inheritedObligations(kab, Y3 ) = { c }. inheritedObligations(kab, Y4 ) = { d }.
´ DE COMPLETITUD 6.2. DEMOSTRACION
65
Definici´ on 32 (inheritedObligations(α, X ′ )). inheritedObligations : (ΣR ∪ {τ })∗ × δ → ℘(suf ijos(LM )) inheritedObligations(α, X) = z|ΣR | z ∈ (ΣR ∪ { τ })∗ · z|ΣR 6= ǫ ∧ | {z } la obligaci´on contin´ ua ∃u, v, y ∈ (ΣR ∪ { τ })∗ · α = uvy ∧ v| ∈ L ∧ | ΣR{z P} vali´o el Prechart antes y|ΣR 6= ǫ ∧ | {z } el Prechart vali´o antes de completar α ∃γ ∈ (ΣR ∪ { τ })∗ · γ|ΣR ∈ LM ∧ yz = γ ∧ | {z } transitando por una obligaci´ on que puede completarse desde este punto z X =⇒} | {z se on tiene que poder completar desde X la obligaci´ Con esta relaci´on as´ı definida, se est´an relacionando los estados de W que tienen obligaciones con los de X que pueden cumplirlas. Es decir vale que para cualquier par (W ′ , X ′ ) en la relaci´on, las obligaciones en W ′ pueden completarse desde X ′ . Teorema 10 (Toda obligacion en W ′ puede completarse desde X ′ ). Sea (W ′ , X ′) ∈ RW,X@ΣR : θ ∀θ ∈ obligaciones(W0′ ) =⇒ X ′ =⇒p Demostraci´on. Ver Ap´endice A.3.1
6.2.2.
Demostraci´ on de relaci´ on de refinamiento d´ ebil
A continuaci´on una demostraci´on de que la relaci´on antes definida es efectivamente una relaci´on de refinamiento. on de refinamiento Teorema 11. RW,X@ΣR es una relaci´ Demostraci´on. Hay que probar dos cosas. El par (W, X@ΣR ) est´a en la relaci´on. Y cada par en la relaci´on cumple los dos puntos de la Definici´on 10. Veamos que (W, X@ΣR ) ∈ RW,X@ΣR :
66
CAP´ITULO 6. COMPLETITUD DEL ALGORITMO DE S´INTESIS α
α
Si consideramos α = ǫ vale que X@ΣR =⇒ X@ΣR y W =⇒ W . Adem´as obligaciones(W0 ) = ǫ = newObligations(α), entonces el par est´a en la relaci´on. Lo que hay que probar ahora es que cualquier par en la relaci´on cumple los dos puntos de la Definici´on 10. Sea (W ′ , X ′ ) ∈ RW,X@ΣR , entonces existe un α tal α α que X@ΣR =⇒ X ′ y W =⇒ W ′ . ℓ
Sea ℓ ∈ ΣR ∪ { τ } tal que X ′ −→p X ′′ hay que probar que existe un W ′′ ℓˆ
tal que W ′ =⇒p W ′′ ∧ (W ′′ , X ′′ ) ∈ RW,X@ΣR . Caso ℓ = τ . Si X ′′ sigue pudiendo completar las obligaciones de W ′ (si existieran), como ℓˆ
vale W ′ =⇒p W ′ entonces W ′ es el W ′′ buscado ya que (X ′′ , W ′ ) est´a en la relaci´on. Si, en cambio, hay obligaciones de W ′ que X ′′ ya no puede completar entonces se toma como W ′′ al que se llega transitando por τ desde W ′ (existe pues hay una transici´on requerida desde W ′ ). Las u ´ nicas obligaciones de ′′ W ser´an entonces newObligations(αℓ), entonces el par est´a en la relaci´on. Supongamos a partir de ahora que ℓ 6= τ . Si ℓ no es parte de una obligaci´on de W ′ entonces hay una transici´on maybe αℓ por ℓ a un W ′′ (con lo cual W =⇒p W ′′ ) y tendr´a como obligaciones a newObligations(α) con lo cual (W ′′ , X ′′ ) est´a en la relaci´on. Si en W ′ hay una obligaci´on θ, entonces por el Teorema 10 se que puede completarse desde X ′ . Puede suceder que X ′′ no sea parte de un camino que complete la obligaci´on con lo cual puedo tomar la transici´on τ desde W ′ a un W ′′ (existe pues el algoritmo agrega transiciones τ cuando hay obligaciones) y las obligaciones αℓ de W ′′ ser´an simplemente newObligations(αℓ) y adem´as W =⇒p W ′′ entonces (W ′′ , X ′′ ) est´a en la relaci´on. Si, en cambio, X ′′ es parte de un camino que completa la obligaci´on θ = ℓθ′ ℓ entonces W ′ −→r W ′′ y las obligaciones de W ′′ ser´an newObligations(αℓ) y la heredada θ′ si y solo si θ′ 6= ǫ. Si θ′ = ǫ entonces W ′′ solo tiene obligaciones nuevas y resulta (X ′′ , W ′′) est´a en la relaci´on. Pero si θ′ 6= ǫ entonces est´a en inheritedObligations(αℓ, X ′′ ,) ya que θ pod´ıa completarse desde X ′ pasando por X ′′ y la obligaci´on a´ un no se ha consumido. Entonces (X ′′ , W ′′ ) est´a en la relaci´on. ℓ
Sea ℓ ∈ ΣR (en W no hay transiciones requeridas por τ ) tal que W ′ −→r W ′′ ℓˆ
hay que probar que existe un X ′′ tal que X ′ =⇒r X ′′ ∧ (W ′′ , X ′′ ) ∈ RW,X@ΣR .
´ DE COMPLETITUD 6.2. DEMOSTRACION
67
ℓ es una transici´on requerida de W’ con lo cual es parte de una obligaci´on θ = ℓθ′ . Como (W ′, X ′ ) est´a en la relaci´on, por el Teorema 10 θ puede completarse desde X ′ , es decir, θ ∈ inheritedObligations(α, X ′ ). Esto significa ℓ
θ′
que existe un X ′′ tal que X ′ =⇒r X ′′ =⇒r . Las obligaciones de W ′′ , adem´as de newObligations(αℓ) tienen como obligaci´on heredada a θ′ si y solo si θ′ 6= ǫ. Si θ′ es ǫ entonces las obligaciones de W ′′ son simplemente newObligations(αℓ) y entonces el par (W ′′ , X ′′ ) est´a en la relaci´on. Si, por el contrario, θ′ 6= ǫ entonces θ′ ∈ inheritedObligations(αℓ, X ′′ ) y entonces (W ′′ , X ′′ ) est´a en la relaci´on.
68
CAP´ITULO 6. COMPLETITUD DEL ALGORITMO DE S´INTESIS
Cap´ıtulo 7 Caso de estudio “Vi infinitos procesos que formaban una sola felicidad, y, entendi´endolo todo, alcanc´e tambi´en a entender la escriturad del tigre.” La escritura del dios - Jorge Luis Borges
7.1.
Mine Pump
En esta secci´on se describe el caso de estudio que fue realizado al modelar el controlador de una bomba funcionando en una mina [19]. En este sistema, el controlador de la bomba se usa para evitar que el nivel del agua supere un cierto umbral y de esta manera inunde la mina. Pero para evitar el riesgo de una explosi´on, la bomba solo deber´ıa ser prendida si no hay gas metano presente en ella. El controlador observa los niveles de agua y metano utilizando sensores y controla la bomba a fin de garantizar las condiciones de seguridad de la mina.
7.2.
Metodolog´ıa
El caso de estudio se condujo realizando iteraciones sobre el esquema sintetizaranalizar-relevar. Primero, un MTS se sintetiza a partir de propiedades conocidas y escenarios. El lenguaje de escenarios utilizado es epLSC y se utiliza el algoritmo presentado en este trabajo para sintetizar un MTS que caracteriza todos 69
CAP´ITULO 7. CASO DE ESTUDIO
70
los LTS que satisfacen el escenario. Para describir las propiedades se utiliza l´ogica temporal lineal de fluents [15] para lo cual existe un algoritmo de s´ıntesis que construye un MTS que caracteriza todos los LTS que satisfacen la propiedad [12]. La composici´on de los MTS sintetizados de epLSCs y propiedades FLTL [15] se hace usando merge de MTS. En la siguiente etapa, el comportamiento maybe del MTS resultante es analizado con el fin de identificar comportamiento prohibido y requerido faltante. El an´alisis es usando t´ecnicas de validaci´on basadas en modelos como inspecci´on (usando la representaci´on gr´afica y abstracta de los MTS), animaci´on, y minimizaci´on. Para realizar dicho an´alisis se utiliz´o, como soporte, la herramienta MTSA (Modal Transition System Analyser). Finalmente, la exploraci´on del comportamiento llev´o a la tercer etapa en la cual nuevas propiedades y escenarios son relevados en base al conocimiento disponible sobre el dominio del problema. En este caso de estudio se utiliz´o la documentaci´on existente del controlador de la bomba en reemplazo del experto en el dominio.
7.3.
Iteraciones
El caso de estudio comienza a partir de los escenarios descriptos por los descriptos en las Figuras 7.1 y 7.2. Las acciones que se utilizan son las del conjunto A de la Figura 7.4. El esenario 1 ejemplifica el comportamiento de la bomba prendi´endose cuando el nivel de agua es alto, el metano est´a por debajo del nivel cr´ıtico y la bomba est´a apagada. En este caso, siempre que sucedan los eventos switchOf f , methLeaves y highW ater, en cualquier orden (pues est´an en una co-regi´on), debe ser posible que suceda a continuaci´on la secuencia descripta por el Mainchart (con la posibilidad que suceda en medio cualquier evento fuera del scope del diagrama). El algoritmo de s´ıntesis aplicado a este escenario genera un MTS de 18 estados. El escenario 2(Figura 7.2) provee un ejemplo del apagado de la bomba cuando el nivel de metano supera el nivel cr´ıtico y la bomba est´a prendida. Debe ser posible que la bomba se apague, el metano se vaya y luego se vuelva a prender la bomba. El MTS producto de aplicar el algoritmo de s´ıntesis se ve en la Figura 7.3. Adem´as de los escenarios se utilizan dos propiedades que debe cumplir el
7.3. ITERACIONES
71
Figura 7.1: Escenario 1 del Mine Pump
Figura 7.2: Escenario 2 del Mine Pump sistema que controla el Mine Pump(Figura 7.5): evitar inundaciones φ1 : “si no hay metano y el nivel del agua es alto, la bomba debe estar prendida en el siguiente estado” prevenir una explosi´on
72
CAP´ITULO 7. CASO DE ESTUDIO
Figura 7.3: MTS sintetizado a partir del escenario de la Figura 7.2 φ2 : “si se detecta metano entonces la bomba debe estar apagada en el siguiente estado” Estas propiedades versan sobre los siguientes fluents (Figura 7.4): HighWater que es verdadero cuando el agua est´a alta
LowWater es verdadero cuando el agua est´a baja
PumpOn es verdadero cuando la bomba est´a encendida
Methane que es verdadero cuando el metano supera el l´ımite de seguridad
7.3. ITERACIONES
73
En este caso, los escenarios 1 y 2 funcionan como testigos de estas propiedades, proveen ejemplos de como el sistema podr´ıa lograr estas propiedades. Es interesante notar el impacto de la decisi´on de especificar estos escenarios con sem´antica existencial en lugar de universal. Por ejemplo, si se hubiera hecho un diagrama similar al 1 pero con la forma de un uLSC implicar´ıa, entre otras cosas, que no puede aparecer metano antes de prender la bomba. Esto es algo demasiado fuerte para una etapa tan temprana de modelado. En el caso del escenario 2, si se hubiera optado por un uLSC el Maichart siempre deber´ıa suceder luego del Prechart, y esto implica que luego del apagar la bomba y que el metano se fue no puede reaparecer antes de prender la bomba (porque methAppears es parte del scope). Es decir, la traza switchOn methAppers switchOff methLeaves methAppears methLeaves switchOn no satisface un uLSC con los diagramas del escenario 2 pero si podr´ıa ser parte de un modelo que satisfaga el epLSC de dicho escenario. Claramente no es deseable restringir ese comportamiento ya que es propio del ambiente y no del controlador de la bomba. = {switchOn, switchOff, methAppears, methLeaves, medWater, highWater, lowWater} HighWater = hhighWater, {lowWater, medWater}i LowWater = hlowWater, {medWater, highWater}i PumpOn = hswitchOn, switchOffi Methane = hmethAppears, methLeavesi A
Figura 7.4: Fluents y acciones iniciales para el caso de estudio φ1 = G((HighWater ∧ ¬MethanePresent) ⇒ X PumpOn) /* La bomba debe estar prendida si el agua est´a alta y no hay metano */ φ2 = G((LowWater ∨ MethanePresent) ⇒ X ¬PumpOn) /* La bomba debe ser apagada si hay agua baja o no hay metano */ Figura 7.5: Propiedades iniciales para el caso de estudio El resultado de la primer iteraci´on es un modelo M1 que surge del merge entre los MTS sintetizados a partir de los escenarios 1 y 2, y las propiedades φ1 y φ2 . El merge que hace la herramienta MTSA es menos eficiente cuando trata con MTSs con distintos alfabetos. Por ello, la estrategia utilizada es primero generar un par de MTSs M1a y M1b donde el primero es el merge entre el escenario 1 y la propiedad φ1 y M1b es el resultado del merge entre el escenario 2 y la propiedad φ2 . Los MTSs generados a partir de las propiedades tienen el alfabeto completo
74
CAP´ITULO 7. CASO DE ESTUDIO
del caso de estudio con lo cual M1a y M1b tienen el mismo alfabeto y el merge entre ellos (que genera M1 ) es m´as eficiente que haber hecho merge en cualquier otro orden arbitrario entre los 4 MTSs. Analizando M1 se descubre comportamiento no deseado de acciones controladas por el ambiente. Por ejemplo el agua pasando del nivel alto (highW ater) a bajo (lowW ater) sin pasar por el nivel medio (medW ater). Tambi´en puede prenderse la bomba cuando ya est´a prendida. A continuaci´on una traza posible de M1 : lowWater? highWater? switchOn? switchOn? medWater? switchOn? highWater? switchOff ? lowWater? lowWater?. Entonces se modelan tres componentes que conforman el ambiente y que se componen en paralelo con el resultado de la iteraci´on anterior: W aterLevelSensor, MethaneSensor, P ump. W aterLevelSensor modela el sensor de agua y es consistente con la forma en la cual se espera que cambie el nivel del agua entre bajo, medio y alto. MethaneSensor modela el sensor que indica si hay gas presente en la mina. Finalmente, P ump modela la bomba (el aparato bomba de agua) que puede ser encendida y apagada. Los LTSs para estos componentes se ven en la Figura 7.6.
Figura 7.6: LTSs del ambiente y el aparato bomba Entonces si se ponen en paralelo estos componentes y luego se compone el resultado en paralelo con el MTS de la primer iteraci´on se llega a M2 . De esta manera se logra respetar el comportamiento esperado de los 3 componentes modelados en la Figura 7.6.
7.3. ITERACIONES
75
En este nuevo modelo se aprecia que, a veces, est´a como u ´ nica transici´on apagar la bomba y no es posible que aparezca metano (antes de apagarla). Esto no es deseable que suceda en una iteraci´on tan temprana. Podr´ıa ser peligroso suponer que eso no puede suceder. Fue producto de haber impuesto restricciones demasiado fuertes. Esto sucede porque las propiedades φ1 y φ2 son demasiado fuertes, ya que utilizan el operador next de la l´ogica temporal. En particular, esto fuerza la presencia de urgencia (inmediata), que hace que haya comportamiento no deseado en el resultado de los merge y composiciones. Estas propiedades se relajan creando dos nuevas que las reemplazan: φ′1 y φ′2 (Figura 7.7). φ′1 = G((HighWater ∧ ¬MethanePresent) U tick ⇒ ¬tick U PumpOn) φ′2 = G((LowWater ∨ MethanePresent) U tick ⇒ ¬tick U ¬PumpOn) Figura 7.7: Propiedades φ1 y φ2 relajadas Lo que se necesita es una noci´on m´as d´ebil de urgencia. Una que todav´ıa fuerze la pol´ıticas de seguridad del controlador de la mina: evitar que se inunde y evitar una explosi´on. Por ejemplo, en lugar de pedir que la bomba se prenda tan pronto como se satisfacen ciertas condiciones, se pide que eso suceda antes de un determinado lapso de tiempo. Por lo tanto se modela expl´ıcitamente el tiempo mediante el evento tick. El evento tick se utiliza para representar el paso del tiempo en un reloj global del sistema. Los requerimientos temporizados utilizar´an ese tick para sincronizar y para dar prioridad a ciertas tareas. Este enfoque es una manera com´ un de modelar tiempo discreto en formalismos basados en eventos [20]. Entonces las nuevas propiedades relajadas utilizan el evento tick de los FLTL asincr´onicos [21], utilizada para indicar paso del tiempo. En particular φ′1 dice que si se da el caso en el cual no hay metano y el agua est´a alta en un cierto momento, entonces la bomba tiene que ser prendida antes del siguiente evento tick. Y φ′2 dice que cuando haya metano o el agua est´e baja durante un cierto tiempo, la bomba debe ser apagada antes del siguiente tick. Es decir, estas propiedades permiten que, mientras valgan las condiciones, se cumpla lo requerido antes del siguiente tick, pudiendo suceder eventos en el medio. Para obtener el nuevo modelo M3 hay que primero conseguir un MTS que satisfaga las propiedades (φ′1 y φ′2 ) y tambi´en los escenarios, y luego, componerlo con la composici´on de las tres m´aquinas que modelan el ambiente y la bomba como se hizo en M2 .
76
CAP´ITULO 7. CASO DE ESTUDIO
Al hacer merge de los MTS generados a partir de las propiedades y los escenarios (estos u ´ ltimos mediante el Algoritmo 1), adem´as de preservar las propiedades, sus implementaciones satisfacen los escenarios. Esto sucede porque el modelo resultante es refinamiento de los sintetizados a partir de los escenarios, y el refinamiento preserva implementaciones. Entonces, como toda implementaci´on del sintetizado satisface el escenario, tambi´en lo hacen las implementaciones de sus refinamientos. Para la u ´ ltima iteraci´on se parti´o de un nuevo escenario, el escenario 3 de la Figura 7.8, que provee m´as informaci´on sobre el apagado de la bomba, en este caso, cuando el nivel del agua en la mina es bajo. Esto es para evitar alg´ un da˜ no en la bomba al tratar de bombear agua cuando no hay. A partir del escenario 3
Figura 7.8: Escenario 3 del Mine Pump se sintetiza el MTS de la Figura 7.9 utilizando el Algoritmo 1. Luego se hace un merge entre este modelo y M3 para obtener M4 , que satisface adem´as, el nuevo escenario. Este escenario inici´o una discusi´on sobre cual ser´ıa una precondici´on adecuada para el apagado de la bomba. Se consideraron tres posibles estrategias: la bomba se mantiene prendida mientras haya agua; o se apaga en cuanto el nivel baje de alto; o minimiza el cambio de estados, es decir que si est´a prendida se queda as´ı hasta que el nivel est´e bajo, y si est´a apagada as´ı se queda hasta que el nivel est´e alto.
7.3. ITERACIONES
77
Figura 7.9: MTS sintetizado a partir del escenario de la Figura 7.8 Se opt´o por la primer opci´on lo cual llev´o a la creaci´on de las propiedades φ3 y φ4 (Figura 7.10): φ3 : “agua baja es la precondici´on para apagar la bomba” φ4 : “la bomba debe ser prendida inmediatamente despu´es que el nivel del agua no est´e bajo y no haya metano” El u ´ ltimo modelo, M5 es el merge de M4 con estas dos u ´ ltimas propiedades; a saber:φ3 y φ4 . Este nuevo modelo satisface todos los escenarios y las propiedades hasta aqu´ı descriptas. Pero lo m´as interesante es que a partir de ´el se puede continuar este proceso asegurando que los modelos resultantes satisfacen los escenarios y las propiedades. φ3 = G(XswitchOf f ⇒ (MethanePresent ∨ LowWater)) φ4 = G((¬LowWater ∧ ¬MethanePresent) U tick ⇒ ¬tick U PumpOn) Figura 7.10: Propiedades φ3 y φ4
78
CAP´ITULO 7. CASO DE ESTUDIO
Cap´ıtulo 8 Conclusiones “Que muera conmigo el misterio que est´a escrito en los tigres. Quien ha entrevisto el universo, quien ha entrevisto los ardientes designios del universo, no puede pensar en un hombre, en sus triviales dichas o desventuras, aunque ese hombre sea ´el. Ese hombre ha sido ´el, y ahora no le importa. Qu´e le importa la suerte de aquel otro, qu´e le importa la naci´on de aquel otro, si ´el, ahora, es nadie. Por eso no pronuncio la f´ormula, por eso dejo que me olviden los d´ıas, acostado en la oscuridad.” La escritura del dios - Jorge Luis Borges
8.1.
Contribuciones
En esta tesis se defini´o un lenguaje de escenarios con sem´antica existencial (epLSC) que permite la especificaci´on de comportamiento condicional. Esta sem´antica est´a alineada con los enfoques de ingenier´ıa de requerimientos basados en casos de uso y escenarios. Encaja y se complementa con los uLSCs mejor que los eLSCs, ya que ´estos u ´ ltimos carecen de Precharts y su sem´antica es demasiado d´ebil como para expresar escenarios interesantes. Esta mejor correspondencia entre epLSC y uLSC nos acerca al objetivo de proveer un framework unificado para pasar de descripciones que representan ejemplos de ejecuciones del sistema a descripciones completas del comportamiento del mismo a trav´es del proceso de relevamiento de requerimientos. Adem´as se defini´o un algoritmo de s´ıntesis para construir, a partir de un epLSC, un MTS. El algoritmo se demostr´o correcto y completo. Esto significa 79
80
CAP´ITULO 8. CONCLUSIONES
que este MTS caracteriza, mediante la noci´on de refinamiento, a todos los LTS que satisfacen el escenario. Entonces se puede analizar y refinar el MTS con la seguridad de preservar la satisfacci´on de los escenarios. Se implement´o el algoritmo en Java. Dicha implementaci´on fue utilizada para sintetizar los MTS a partir de los diagramas usados en esta tesis. La manera de ingresar los diagramas es describiendo los conjuntos LP y LM en archivos de entrada con un formato muy simple y como salida genera un proceso FSP (Finite State Process) que representa al MTS y puede ser ingresado en, por ejemplo, la herramienta MTSA para ver el MTS resultante.
8.2.
Trabajos relacionados
Existe una variedad de notaciones basadas en escenarios desarrolladas con diversas cualidades y sem´anticas. La discusi´on se enfoca en aquellos con caracter´ısticas que se relacionan con el Prechart del epLSC. El uso de Prechart o triggers para aumentar la expresividad de diagramas de secuencia ha sido investigado por varios autores. Sin embargo, todos estos enfoques tienen una sem´antica universal. Kr¨ uger [2] extiende los MSC con triggers asignandoles una sem´antica universal: si un cierto patr´on A ocurre en el sistema, entonces otro patr´on B es inevitable. Sengupta y Cleaveland [8] tambi´en proponen un mecanismo con triggers cuya interpretaci´on es universal, pero los triggers (y lo que desencadenan) se especifica para cada componente en particular, en lugar del conjunto de componentes como es el caso de los LSC. En la formulaci´on original de los LSCs [18], Damm y Harel introducen Precharts para las dos modalidades presentadas: existenciales y universales. Pero la sem´antica de un LSC existencial con un Prechart P y Mainchart M resulta ser equivalente a la de un existencial con un Mainchart P M y sin Prechart. Por lo tanto, en ese caso, el Prechart en la modalidad existencial solo es una cuesti´on sint´actica y no aporta ninguna expresividad. Esto llev´o a que en futuros desarrollos de LSCs(e.g. [5, 22]) el Prechart para los eLSC fuera removido. La sem´antica de los epLSC puede ser pensada como un fragmento de la l´ogica temporal branching CTL∗ . Informalmente, son equivalentes a la f´ormula AG(p → E m) donde p y m codifican el lenguaje del Prechart y Mainchart. Efectivamente,
8.2. TRABAJOS RELACIONADOS
81
la sem´antica no puede ser formulada en t´erminos de la l´ogica temporal l´ıneal LTL, o trazas, como si puede hacerse con los uLSC y eLSC en [5] o los triggered MSC en [2]. Cuando vale el Prechart en un epLSC se activa la parte existencial y se espera que todo el comportamiento del Mainchart pueda ser provisto por el sistema. Entonces la noci´on existencial de estos diagramas est´a en la l´ınea de la interpretaci´on existencial de los MSC y difiere de la de los eLSC. Un MSC interpretado existencialmente requiere que todas las trazas que describe est´en en el sistema. Un eLSC solo requiere que alguna de sus trazas est´e en el sistema. Muchos enfoques de especificaciones basadas en escenarios proveen algor´ıtmos de s´ıntesis que producen modelos. El resultado de la s´ıntesis puede ser alguno de los modelos que satisface el escenario que le dio origen, o uno que caracterice, a trav´es de alguna noci´on de refinamiento, a todos los modelos que satisfacen el escenario. Dado un escenario con interpretaci´on existencial, solo es posible sintetizar un modelo M que represente la cota inferior del comportamiento esperado del sistema, es decir M hace lo menos posible a la vez que asegura el comportamiento descripto por el escenario. Este modelo caracteriza mediante inclusi´on de trazas o simulaci´on a todos los modelos de comportamiento que satisfacen el escenario: si N puede simular o incluye las trazas de M, entonces satisface el escenario. Enfoques como los de [3, 17] proveen algoritmos de s´ıntesis de esta caracter´ıstica. Por otro lado, dado un escenario universal, es posible sintetizar un modelo M que haga tanto como pueda preservando el escenario. Este modelo funciona como una cota superior del comportamiento esperado del sistema y puede decirse que caracteriza todos los modelos que satisfacen el escenario: Si N es simulado por M, entonces N satisface la descripci´on del escenario universal. Este tipo de enfoque es el de, por ejemplo, [5] para los uLSC y [8]. En [12] se muestra que modelos de comportamiento tradicionales, bivaluados, como los LTS o statecharts no pueden modelar adecuadamente descripciones que contengan afirmaciones exitenciales y universales juntas como en una combinaci´on de eLSCs y uLSCs. Es decir, no es posible construir un LTS, por ejemplo, que caracterice todos los LTS que satisfacen la descripci´on con modalidad mezclada. Intuitivamente, esto es porque el refinamiento de modelos de comportamiento tradicionales pueden interpretar el modelo como una cota superior o inferior del comportamiento esperado del sistema, pero no pueden proveer ambas cotas simultaneamente. Por ello, los enfoques que apuntan a sintetizar a partir de combinaciones de escenarios existenciales y universales est´an limitados a ejemplos de modelos de comportamiento que satisfacen el escenario. Este es el caso de
CAP´ITULO 8. CONCLUSIONES
82
algoritmos de los algoritmos de s´ıntesis aportados en [23] y [24]. En esta tesis se utiliza un modelo de comportamineto trivaluado, un MTS, como resultado de la s´ıntesis. Esto es un avance en cuanto a expresividad que permite un algoritmo de s´ıntesis generador de un modelo que caracteriza todos los LTSs que satisfacen un epLSC. Este tipo de resultados no puede obtenerse sintetizando modelos de comportamiento bivaluados, como LTS. Esto es debido a su incapacidad de describir cotas inferiores y superiores simultaneamente: si el sistema satisface el Prechart (cota superior, no es obligatorio que el sistema lo haga) entonces el sistema tiene que poder realizar el Mainchart (cota infrior, el sistema lo requiere) pero pudiendo presentar tambi´en otro comportamiento (cota superior, no es requerido que lo haga).
8.3.
Trabajo futuro
En el futuro se espera incluir en los diagramas f´ormulas FLTL como condiciones mezcladas entre los mensajes. Esto los har´ıa m´as entendibles ya que mediante una f´ormula se pueden codificar secuencias de eventos que satisfacen la condici´on de una manera m´as compacta. Tambi´en se analizar´a la s´ıntesis de MTS a partir de un uLSC. No es claro si existe un MTS que caracterice, mediante refinamiento, a todos los LTS que satisfacen un uLSC. Hay que estudiar tambi´en variantes de MTS como OneSelecting MTS y Disjuntive MTS ya que, quiz´as, sea alguna de ellas la ideal como resultado de s´ıntesis de un uLSC. Dotar a MTSA de una interfaz para dibujar LSC e integrar la implementaci´on del algoritmo de s´ıntesis ser´ıa algo deseable. De esta manera se podr´an dibujar los epLSC directamente en la herramienta y obtener el MTS sintetizado. Se espera utilizar los epLSC en casos de estudio m´as grandes para continuar validando la t´ecnica desarrollada.
Appendices
83
Ap´ endice A Demostraciones A.1.
Modelos
A.1.1.
Demostraci´ on Teorema 1
Sean M, N ∈ δ (de trazas infinitas) tal que M N donde R ⊆ δ × δ es la relaci´on de refinamiento y αM = αN = Σ. Para cuaquier β ∈ (Σ ∪ { τ })+ : β
β|Σ
M −→r M ′ =⇒ (∃N ′ · N =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R) β
β|Σ
N −→p N ′ =⇒ (∃M ′ · M =⇒p M ′ ∧ (M ′ , N ′ ) ∈ R) Demostraci´on. Se demuestra la primer regla, la segunda es an´aloga. Se har´a por β inducci´on en la longitud de β. Supongamos que M −→r M ′ . Hay que probar β|Σ
∃N ′ · N =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R
Base: |β| = 1. Como la longitud es 1, β ∈ Σ ∪ { τ }. Pero entonces βˆ = β|Σ ya que β|Σ = ǫ si β = τ y β|Σ = β si β 6= τ . βˆ
β
Como M −→r M ′ , por la Definici´on 10 entonces ∃N ′ · N =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R. Adem´as β|Σ = βˆ entonces reemplazando en la ecuaci´on anterior obtenemos lo buscado. Paso inductivo: |β| > 1. β = γℓ, ℓ ∈ Σ ∪ { τ }. 85
´ APENDICE A. DEMOSTRACIONES
86 γ
ℓ
γ
Existe un Mγ · M −→r Mγ −→r M ′ . Por H.I, como Mγ · M −→r Mγ γ|Σ
entonces ∃Nγ · N =⇒r Nγ ∧ (Mγ , Nγ ) ∈ R ℓ Como (Mγ , Nγ ) ∈ R y Mγ −→r M ′ , seg´ un la Definici´on 10 entonces ∃N ′ · ℓˆ Nγ =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R. Pero ℓˆ = ℓ|Σ con lo cual se puede reemplazar en la ecuci´on anterior. γ|Σ ℓ|Σ Uniendo todo tenemos que ∃N ′ · N =⇒r Nγ =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R que γℓ|Σ
implica ∃N ′ · N =⇒r N ′ ∧ (M ′ , N ′ ) ∈ R.
A.2.
Correcci´ on
A.2.1.
Lemas
Lema 1. Sea α un sufijo significativo, a ∈ ΣR ∪ { τ }, β ∈ (ΣR ∪ { τ })+ next(α, βa) = suf ijoSignif icativo(next(α, β)a) Demostraci´on. Por inducci´on en la longitud de β. Caso base: |β| = 0, es decir β = ǫ next(α, βa) = next(α, a) = next(suf ijoSignif icativo(αa), ǫ) = suf ijoSignif icativo(αa) | {z } por definici´on de next
Pero adem´as vale α = next(α, ǫ) = next(α, β) (tambi´en por definici´on de next y β). Entonces suf ijoSignif icativo(αa) = suf ijoSignif icativo(next(α, β)a). Y es lo que se quer´ıa probar. Caso |β| > 0, es decir β = tβ ′ donde t ∈ ΣR . next(α, tβ ′ a) = next(suf ijoSignif icativo(αt), β ′ a) = | {z } definici´on de next
= suf ijoSignif icativo(next(suf ijoSignif icativo(αt)β ′ , a)) = | {z } por H.I.
´ A.2. CORRECCION = suf ijoSignif icativo(
87 next(α, tβ ′ ) | {z }
a).
next(suf ijoSignif icativo(αt),β ′ )
Lema 2. Sea κ ∈ (ΣR ∪ { τ })∗ , a ∈ ΣR suf ijoSignif icativo(suf ijoSignif icativo(κ)a) = suf ijoSignif icativo(κa) Demostraci´on. El sufijo significativo de la palabra κ es simplemente el sufijo m´as largo que est´a en pref ijos(LP ). Es decir es tambi´en un prefijo de LP . Sea κ = κ0 . . . κi κi+1 . . . κn , y suf ijoSignif icativo(κ) = κi κi+1 . . . κn Supongamos que suf ijoSignif icativo(κa) comienza en κj con j < i. Entonces κj κj+1 . . . κi . . . κi+1 κn a es prefijo de una palabra de LP , con lo cual κj κj+1 . . . κi . . . κi+1 κn tambi´en es prefijo de esa palabra. Pero esto es absurdo ya que suf ijoSignif icativo(κ) = κi κi+1 . . . κn , y por definici´on no hay un sufijo m´as largo que κi κi+1 . . . κn que sea prefijo de una palabra de LP . Entonces suf ijoSignif icativo(κa) nunca puede ser un sufijo que supere κi con lo cual suf ijoSignif icativo(κa) = suf ijoSignif icativo(κi κi+1 . . . κn a) = suf ijoSignif icativo(suf ijoSignif icativo(κ)a)
A.2.2.
Demostraci´ on Teorema 2
Sea α un sufijo significativo, γ, β ∈ (ΣR ∪ { τ })∗ next(α, γβ) = suf ijoSignif icativo(next(α, γ)β) Demostraci´on. Por inducci´on en la longitud de β. Caso base: |β| = 0, es decir β = ǫ next(α, γβ) = next(α, γ) Adem´as: suf ijoSignif icativo(next(α, γ)β) = suf ijoSignif icativo(next(α, γ)ǫ) = suf ijoSignif icativo( next(α, γ) )= | {z } es un sufijo significativo = next(α, γ) | {z } por Propiedad 3
´ APENDICE A. DEMOSTRACIONES
88
Caso |β| > 0, es decir β = β ′ a con a ∈ ΣR next(α, γβ) = next(α, γβ ′ a) = = suf ijoSignif icativo(next(α, γβ ′ )a) = | {z } por Lema 1
= suf ijoSignif icativo(suf ijoSignif icativo(next(α, γ)β ′ )a) = {z } | por H.I. = suf ijoSignif icativo(next(α, γ)β ′ a) = | {z } por Lema 2
= suf ijoSignif icativo(next(α, γ)β)
A.2.3.
Demostraci´ on Teorema 4
Sea W = (S, Σ, ∆r , ∆p , s0 ) el MTS resultante del Algoritmo 1 y < α, Θ >∈ S ∀β ∈ (ΣR ∪ { τ })∗ · β|ΣR ∈ LP =⇒ β
∀ < α′ , Θ′ >∈ S · (< α, Θ >−→< α′ , Θ′ > =⇒ suf ijos(α′) ∩ LP 6= ∅)
Demostraci´on. El estado al cual se llega tiene como sufijo significativo a next(α, β), es decir next(α, β) = α′ . Pero por el Corolario 3 next(α, β) = suf ijoSignif icativo(αβ) = α′ . Por la Definici´on 28 de sufijo significativo vale: α′ = m´ax|γ| { γ | αβ = zγ ′ ∧ γ ′ |ΣR = γ ∧ γ ∈ pref ijos(LP ) } Pero β cumple β|ΣR ∈ pref ijos(LP ) y adem´as es un sufijo de αβ con lo cual est´a en el conjunto { γ | αβ = zγ ′ ∧ γ ′ |ΣR = γ ∧ γ ∈ pref ijos(LP ) } Pueden suceder dos cosas, o bien β|ΣR es el sufijo significativo, o hay uno m´as largo. Pero si hay uno m´as largo tiene que tener el sufijo β|ΣR con lo cual β|ΣR ∈ suf ijos(α′). Adem´as, como β|ΣR ∈ pref ijos(LP ), entonces suf ijos(α′ ) ∩ LP 6= ∅.
A.3. COMPLETITUD
A.2.4.
89
Demostraci´ on Teorema 6
Sea W = (S, Σ, ∆r , ∆p , s0 ) el MTS resultante del Algoritmo 1 y < α, Θ >∈ S, θ ∈ Θ ∀β ∈ ΣR · θ = βγ ∧ |β| > 0 =⇒ ′
′
β
∃ < α , Θ >∈ S· < α, Θ >−→r < α′ , Θ′ > ∧ (γ = ǫ ∨ γ ∈ Θ′ ) Demostraci´on. Por inducci´on en la longitud de β.
Caso base: |β| = 1, es decir β ∈ ΣR Por ser una obligaci´on, el algoritmo agrega una transici´on requerida. Es β decir hay un W ′ tal que W =⇒r W ′ . Sea W0′ =< α′ , Θ′ >. Si γ = ǫ no hay nada m´as que probar. Si γ 6= ǫ entonces, como Θ′ = f ollows(Θ, β), γ ∈ Θ′ ya que θ ∈ Θ y θ = βγ. Entonces γ = ǫ ∨ γ ∈ Θ′ . Caso |β| > 1, es decir β = β ′ a con a ∈ ΣR β′
Por H.I W =⇒r W ′ con W0′ =< α′ , Θ′ > y aγ ∈ Θ′ (pues aγ 6= ǫ). Siguiendo a el mismo razonamiento que para el caso base se llega a W ′ =⇒r W ′′ con W0′′ =< α′′ , Θ′′ > y γ = ǫ ∨ γ ∈ Θ′′ β Entonces W =⇒r W ′′ con W0′′ =< α′′ , Θ′′ > y γ = ǫ ∨ γ ∈ Θ′′ .
A.3.
Completitud
A.3.1.
Demostraci´ on Teorema 10
Sea RW,X@ΣR la relaci´on definida en 31, vale que para cualquier par (W ′ , X ′ ), las obligaciones en W ′ pueden completarse desde X ′ Teorema (Toda obligacion en W ′ puede completarse desde X ′ ). Sea (W ′ , X ′ ) ∈ RW,X@ΣR : θ ∀θ ∈ obligaciones(W0′ ) =⇒ X ′ =⇒p α
Demostraci´on. Como el par pertenece a la relaci´on, existe un α tal que X@ΣR =⇒p α|Σ
R ′ X ′ y W =⇒ p W .
90
´ APENDICE A. DEMOSTRACIONES
Sea θ una obligaci´on en W ′ puede ser producto de haber valido el Prechart con α o ser una obligaci´on heredada. Si estamos en el primer caso, es decir θ ∈ newObligations(α), entonces como X satisface el escenario, y al llegar a X ′ se ha satisfecho el Prechart con α, tiene que haber un camino (posiblemente con transiciones τ en el medio) por θ. Es decir θ X ′ =⇒p . Si, en cambio, la obligaci´on θ es una obligaci´on heredada, por como se arma la relaci´on se que θ ∈ inheritedObligations(α, X ′ ) pero entonces por definici´on de θ dicha funci´on vale que se puede completar dicha obligaci´on, es decir X ′ =⇒p .
Ap´ endice B Caso de estudio A continuaci´on el c´odigo utilizado en MTSA durante el caso de estudio. fluent PumpOn = initially False fluent MethanePresent = initially False fluent AtHighWater = initially False fluent AtLowWater = initially True const False = 0 const True = 1 set A = {switchOn, switchOff, methAppears, methLeaves, highWater, lowWater, medWater} // Escemario 2 ESCENARIO2 = (methLeaves? -> ESCENARIO2 |methAppears? -> ESCENARIO2_E_6 |switchOff? -> ESCENARIO2 |switchOn? -> ESCENARIO2_E_4 ), ESCENARIO2_E_2 = (methLeaves -> ESCENARIO2_E_5 |hidden? -> ESCENARIO2 |methAppears? -> ESCENARIO2_E_6 |switchOff? -> ESCENARIO2 |switchOn? -> ESCENARIO2_E_4 91
92
´ APENDICE B. CASO DE ESTUDIO
), ESCENARIO2_E_1 = (switchOff -> ESCENARIO2_E_2 |methLeaves? -> ESCENARIO2 |hidden? -> ESCENARIO2_E_1 |methAppears? -> ESCENARIO2_E_3 |switchOn? -> ESCENARIO2_E_4 ), ESCENARIO2_E_3 = (switchOff -> ESCENARIO2_E_2 |methLeaves? -> ESCENARIO2 |hidden? -> ESCENARIO2_E_3 |methAppears? -> ESCENARIO2_E_6 |switchOn? -> ESCENARIO2_E_1 ), ESCENARIO2_E_4 = (methLeaves? -> ESCENARIO2 |methAppears? -> ESCENARIO2_E_3 |switchOff? -> ESCENARIO2 |switchOn? -> ESCENARIO2_E_4 ), ESCENARIO2_E_5 = (switchOn -> ESCENARIO2_E_4 |methLeaves? -> ESCENARIO2 |hidden? -> ESCENARIO2 |methAppears? -> ESCENARIO2_E_6 |switchOff? -> ESCENARIO2 ), ESCENARIO2_E_6 = (methLeaves? -> ESCENARIO2 |methAppears? -> ESCENARIO2_E_6 |switchOff? -> ESCENARIO2 |switchOn? -> ESCENARIO2_E_1 )\{hidden}. // Escenario 1 ESCENARIO1 = (methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_2 = (medWater -> ESCENARIO1_E_12 |methLeaves? -> ESCENARIO1_E_7 |hidden? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_1
93 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_1 = (methLeaves? -> ESCENARIO1_E_18 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_5 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_3 = (methLeaves? -> ESCENARIO1_E_10 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_9 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_4 = (switchOff -> ESCENARIO1_E_3 |methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_5 = (methLeaves? -> ESCENARIO1_E_6 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_9 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_6 = (switchOn -> ESCENARIO1_E_2 |methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1_E_6 |highWater? -> ESCENARIO1_E_16
94
´ APENDICE B. CASO DE ESTUDIO
|methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_17 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_7 = (methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_14 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_17 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_8 = (switchOn -> ESCENARIO1_E_2 |methLeaves? -> ESCENARIO1_E_10 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1_E_8 |highWater? -> ESCENARIO1_E_11 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_9 = (methLeaves? -> ESCENARIO1_E_15 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_5 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_10 = (methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_16 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_17 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_11 = (switchOn -> ESCENARIO1_E_2 |methLeaves? -> ESCENARIO1_E_15 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1_E_11 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1
95 |switchOff? -> ESCENARIO1_E_5 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_12 = (lowWater -> ESCENARIO1_E_4 |methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |switchOn? -> ESCENARIO1 ), ESCENARIO1_E_17 = (methLeaves? -> ESCENARIO1_E_10 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_11 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_16 = (switchOn -> ESCENARIO1_E_2 |methLeaves? -> ESCENARIO1_E_18 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1_E_16 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_13 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_15 = (switchOn -> ESCENARIO1_E_2 |methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1_E_15 |highWater? -> ESCENARIO1_E_14 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_8 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_14 = (methLeaves? -> ESCENARIO1_E_18 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_1 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_13
96
´ APENDICE B. CASO DE ESTUDIO
|switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_13 = (switchOn -> ESCENARIO1_E_2 |methLeaves? -> ESCENARIO1_E_6 |medWater? -> ESCENARIO1 |hidden? -> ESCENARIO1_E_13 |highWater? -> ESCENARIO1_E_9 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_3 |lowWater? -> ESCENARIO1 ), ESCENARIO1_E_18 = (methLeaves? -> ESCENARIO1_E_7 |medWater? -> ESCENARIO1 |highWater? -> ESCENARIO1_E_14 |methAppears? -> ESCENARIO1 |switchOff? -> ESCENARIO1_E_8 |switchOn? -> ESCENARIO1 |lowWater? -> ESCENARIO1 )\{hidden}. // Propiedades phi 1 y phi 2. Utilizan todo el alfabeto A constraint C_P1 = []((AtHighWater && !MethanePresent) -> X PumpOn)+A constraint C_P2 = []((AtLowWater || MethanePresent) -> X !PumpOn) +A //----------------- ITERACION 1 -----------------// merge entre la propiedad 2 y el escenario 2. ||M_1a = (C_P2 ++ ESCENARIO2). // merge entre la propiedad 1 y el escenario 1. ||M_1b = (C_P1 ++ ESCENARIO1). // M_1 es el resultado de la Iteraci´ on 1. ||M_1 = (M_1a ++ M_1b). //----------------- ITERACION 2 -----------------WaterSensor = LOW, LOW = (medWater -> MIDDLE), MIDDLE = (lowWater->LOW | highWater -> HIGH), HIGH = (medWater -> MIDDLE). MethaneSensor = NOTPRESENT, NOTPRESENT = (methAppears -> PRESENT),
97 PRESENT = (methLeaves->NOTPRESENT). Pump = OFF, OFF = (switchOn -> ON), ON = (switchOff -> OFF). ||Environment = (WaterSensor || MethaneSensor || Pump). // M_2 es el resultado de la Iteraci´ on 2. ||M_2 = (M_1 || Environment).
//----------------- ITERACION 3 -----------------// Nuevo alfabeto con tick set A_With_Tick = {switchOn, switchOff, methAppears, methLeaves, highWater, lowWater, medWater, tick} // Propiedades phi 1 y 2 relajadas (utilizan el tick) constraint C_P1_Relaxed = [](((AtHighWater && !MethanePresent) U tick ) -> (!tick U PumpOn)) + A_With_Tick constraint C_P2_Relaxed = [](((AtLowWater || MethanePresent) U tick ) -> (!tick U !PumpOn)) + A_With_Tick ||M_1a_Relaxed = (C_P2_Relaxed ++ ESCENARIO2). ||M_1b_Relaxed = (C_P1_Relaxed ++ ESCENARIO1). ||M_1_Relaxed = (M_1a_Relaxed ++ M_1b_Relaxed). // M_3 es el resultado de la Iteraci´ on 3. ||M_3 = (M_1_Relaxed || Environment). //----------------- ITERACION 4 -----------------// Escenario 3 minimal Escenario3 = (medWater? -> Escenario3 |highWater? -> Escenario3 |switchOff? -> Escenario3 |switchOn? -> Escenario3_E_6 |lowWater? -> Escenario3_E_2 ), Escenario3_E_2 = (medWater? -> Escenario3 |highWater? -> Escenario3
98
´ APENDICE B. CASO DE ESTUDIO
|switchOff? -> Escenario3 |switchOn? -> Escenario3_E_5 |lowWater? -> Escenario3_E_2 ), Escenario3_E_1 = (medWater -> Escenario3_E_4 |hidden? -> Escenario3 |highWater? -> Escenario3 |switchOff? -> Escenario3 |switchOn? -> Escenario3_E_6 |lowWater? -> Escenario3_E_2 ), Escenario3_E_3 = (switchOff -> Escenario3_E_1 |medWater? -> Escenario3 |hidden? -> Escenario3_E_3 |highWater? -> Escenario3 |switchOn? -> Escenario3_E_5 |lowWater? -> Escenario3_E_2 ), Escenario3_E_4 = (highWater -> Escenario3_E_7 |medWater? -> Escenario3 |hidden? -> Escenario3 |switchOff? -> Escenario3 |switchOn? -> Escenario3_E_6 |lowWater? -> Escenario3_E_2 ), Escenario3_E_6 = (medWater? -> Escenario3 |highWater? -> Escenario3 |switchOff? -> Escenario3 |switchOn? -> Escenario3_E_6 |lowWater? -> Escenario3_E_3 ), Escenario3_E_5 = (switchOff -> Escenario3_E_1 |medWater? -> Escenario3 |hidden? -> Escenario3_E_5 |highWater? -> Escenario3 |switchOn? -> Escenario3_E_6 |lowWater? -> Escenario3_E_3 ), Escenario3_E_7 = (switchOn -> Escenario3_E_6 |medWater? -> Escenario3 |hidden? -> Escenario3 |highWater? -> Escenario3 |switchOff? -> Escenario3
99 |lowWater? -> Escenario3_E_2 )\{hidden}.
||M_4 = (M_3 ++ Escenario3). //----------------- ITERACION 5 -----------------// phi 3 y phi 4 constraint C_P3 = [](X switchOff -> (MethanePresent || AtLowWater)) + A_With_Tick constraint C_P4 = [](((!AtLowWater && !MethanePresent) U tick ) -> (!tick U PumpOn)) + A_With_Tick // M_5 es el resultado de la Iteraci´ on 5 minimal ||M_5 = (C_P4 ++ C_P3 ++ M_4).
100
´ APENDICE B. CASO DE ESTUDIO
Bibliograf´ıa [1] R. Keller. “Formal Verification of Parallel Programs”. CACM, 19(7):371– 384, 1976. [2] I. Kruger. “Distributed system design with message sequence charts”. PhD thesis, Technical University of Munich, 2000. [3] S. Uchitel, J. Kramer, and J. Magee. “Incremental Elaboration of ScenarioBased Specifications and Behaviour Models using Implied Scenarios”. ACM TOSEM, 13(1), 2004. [4] D. Harel and R. Marelly. Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, 2003. [5] Yves Bontemps, Patrick Heymans, and Pierre-Yves Schobbens. From live sequence charts to state machines and back: A guided tour. IEEE Transactions on Software Engineering, 31(12):999–1014, 2005. [6] W. Damm and D. Harel. “LSCs: Breathing Life into Message Sequence Charts.”. FMSD, 19(1):45–80, 2001. [7] ITU. Recommendation z.120: Message sequence charts. ITU, 2000. [8] Bikram Sengupta and Rance Cleaveland. Triggered message sequence charts. IEEE Transactions on Software Engineering, 32(8):587–607, 2006. [9] Konstantinos Zachos, Neil Maiden, and Amit Tosar. Rich-media scenarios for discovering requirements. IEEE Software, 22(5):89–97, 2005. [10] K.G. Larsen and B. Thomsen. “A Modal Process Logic”. In LICS’88, pages 203–210, 1988. [11] S. Uchitel and M. Chechik. “Merging Partial Behavioural Models”. In FSE’04, pages 43–52, 2004. [12] Sebastian Uchitel, Greg Brunet, and Marsha Chechik. Behaviour model synthesis from properties and scenarios. icse, 00:34–43, 2007. 101
102
BIBLIOGRAF´IA
[13] Huttel and Larsen. The use of static constructs in a modal process logic. In LFCS: The 1st International Symposium on Logical Foundations of Computer Science, 1989. [14] Dario Fischbein and Sebastian Uchitel. “On Consistency and Merge of MTS”. In Submitted to International Workshop on Living with Uncertainty, ASE’07, 2007. [15] D. Giannakopoulou and J. Magee. “Fluent Model Checking for Event-Based Systems”. In ESEC/FSE’03, 2003. [16] Sebastian Uchitel, Greg Brunet, and Marsha Chechik. Behaviour model synthesis from properties and scenarios. In ICSE ’07: Proceedings of the 29th International Conference on Software Engineering, pages 34–43, Washington, DC, USA, 2007. IEEE Computer Society. [17] Tewfic Ziadi, Loic Helouet, and Jean-Marc Jezequel. Revisiting statechart synthesis with an algebraic approach. In ICSE ’04: Proceedings of the 26th International Conference on Software Engineering, pages 242–251, Washington, DC, USA, 2004. IEEE Computer Society. [18] Werner Damm and David Harel. Lscs: Breathing life into message sequence charts. In Paolo Ciancarini, Alessandro Fantechi, and Roberto Gorrieri, editors, FMOODS, volume 139 of IFIP Conference Proceedings. Kluwer, 1999. [19] J. Kramer, J. Magee, and M. Sloman. “CONIC: an Integrated Approach to Distributed Computer Control Systems”. IEE Proceedings, 130(1):1–10, 1983. [20] R. Diaz-Redondo, J. Pazos-Arias, and A. Fernandez-Vilas. “Reusing Verification Information of Incomplete Specifications”. In Proceedings of the 5th Workshop on Component-Based Software Engineering, 2002. [21] E. Letier, J. Kramer, J. Magee, and S. Uchitel. “Fluent Temporal Logic for Discrete-time Event-Based Models”. In FSE’05, pages 70–79, 2005. [22] Hillel Kugler, Michael J. Stern, and E. Jane Albert Hubbard. Testing scenario-based models. In Matthew B. Dwyer and Ant´onia Lopes, editors, FASE, volume 4422 of Lecture Notes in Computer Science, pages 306–320. Springer, 2007. [23] Yves Bontemps, Pierre-Yves Schobbens, and Christof L¨oding. Synthesis of open reactive systems from scenario-based specifications. Fundam. Inform., 62(2):139–169, 2004. [24] David Harel and Hillel Kugler. Synthesizing state-based object systems from lsc specifications. Int. J. Found. Comput. Sci., 13(1):5–51, 2002.