arro

Vista previa del material en texto

UNIVERSIDAD DE BUENOS AIRES
FACULTAD DE CIENCIAS EXACTAS Y NATURALES
DEPARTAMENTO DE COMPUTACIÓN
Ejecución de controladores discretos
sintetizados a partir de una especificación
de alto nivel para un robot modelo Lego
NXT y EV3
Tesis presentada para optar al título de
Licenciado en Ciencias de la Computación
Julio M. Arro Fritzler
Co-Directores: Nicolás D’Ippolito Mariano Cerrutti
Buenos Aires, 2014
EJECUCIÓN DE CONTROLADORES DISCRETOS SINTETIZADOS A
PARTIR DE UNA ESPECIFICACIÓN DE ALTO NIVEL PARA UN ROBOT
MODELO LEGO NXT Y EV3
El objetivo de esta tesis es la implementación de técnicas para la generación e imple-
mentación de controladores discretos utilizando como framework de trabajo la herramienta
MTSA aplicado en agentes autónomos utilizando como unidad de control versiones de Lego
NXT y EV3 que permiten el armado de prototipos de manera simple y sencilla en los cua-
les se puede evaluar el comportamiento de controladores sintetizados. Así mismo mostraré
cómo es posible cambiar los modelos permitiendo re configurar los controladores de manera
automática sin necesidad de incurrir en la re escritura de los mismos.
El modelo planteado para cada actor involucrado en el problema, consistirá en máqui-
nas con transiciones etiquetadas (LTS) con propiedades descriptas con lógica lineal tem-
poral que caracterizan las propiedades de seguridad y liveness SGR(1) sobre dominios con
fallas.
Se modelará el problema utilizando como prototipo un robot LEGO MINDSTORM NXT
y EV3. Este tipo de robots provee numerosas ventajas a la hora de crear prototipos tan-
gibles. A lo largo de esta tesis se describirá en detalle la implementación del modelo en
el entorno MTSA incluyendo las extensiones desarrolladas sobre la herramienta para dar
soporte a la robótica y demostrando la calidad de los controladores utilizados y la adapta-
bilidad a cambios de configuración de los sistemas intervinientes abriendo las puertas para
futuros desarrollos combinando robótica con técnicas de síntesis de controladores.
Palabras claves: Síntesis, Control, Cambio de Configuración, Robot planar, LTS, FLTL.
I
ENACTMENT OF A DISCRETE CONTROLLER SYNTHETIZED FROM A
HIGH LEVEL SPECIFICATION TO BE USED WITH A LEGO NXT Y EV3
ROBOTS
pending...
Palabras claves: Controller Synthesis, Change of Configuration, Planar Robot, LTS, FLTL.
II
AGRADECIMIENTOS
Esta tesis esta dedicada especialmente a Mercedes, a mis padres, al equipo de LaFHIS y a
todos los que me han brindado su apoyo y motivación para poder lograr este objetivo tan
anhelado.
III
Índice general
1.. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
2.. Motivación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.1. Controladores LTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.2. Soporte Enactment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.3. Presentación de los casos de estudio . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.4. Resumen de contribuciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2.5. Estructura de la tesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
3.. Fundamentos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3.1. El Mundo y la Máquina . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3.2. Sistemas de Transición Etiquetados . . . . . . . . . . . . . . . . . . . . . . . . . 6
3.3. Lógica Lineal Temporal de Flujos (Fluent Linear Temporal Logic) . . . . . . . 7
3.4. Problemas de control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
3.5. Dominios falibles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
3.6. Procesos de Estados Finitos (FSP) . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
4.. Herramienta MTSA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
4.1. Construcción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
4.2. Análisis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
5.. Motivación Extensión MTSA Tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
5.1. Arquitectura . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
5.2. Enactors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
5.3. Controller / Scheduller . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5.4. Framework Enactment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
5.5. Extensiones – Construcción y registro . . . . . . . . . . . . . . . . . . . . . . . . 22
5.6. Enactors Útiles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
6.. Lego Mindstorm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6.1. Hardware . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6.2. LEJOS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6.3. Construcción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6.4. Driver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6.5. Implementación driver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6.5.1. Comunicación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6.5.2. Control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6.6. Entorno para pruebas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6.7. Robustez – Estadísticas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
6.7.1. Medición . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
6.7.2. Escenario de pruebas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
6.8. Cantidad de operaciones realizadas satisfactoriamente . . . . . . . . . . . . . . 39
6.8.1. Escenario: Luz día . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
IV
6.8.2. Escenario: Tubo fluorescente . . . . . . . . . . . . . . . . . . . . . . . . . 39
6.8.3. Escenario: Luz incandescente . . . . . . . . . . . . . . . . . . . . . . . . . 40
6.8.4. Escenario: Oscuridad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6.8.5. Resumen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
7.. Casos de estudio . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
7.1. 1 robot - Ida y vuelta . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
7.2. Evitando caminos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
7.3. No puede realizar 2 giros a la izquierda . . . . . . . . . . . . . . . . . . . . . . . 48
7.4. Posiciones con recuperación ante falla . . . . . . . . . . . . . . . . . . . . . . . . 50
7.5. 2 robots enemigos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
7.6. Evidencia de ejecución . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
8.. Discusión . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
9.. Conclusiones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
Bibliografía . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
1. INTRODUCCIÓN
En los últimos años ha surgido una prometedora técnica de producción automática de
controladores mediante especificaciones declarativas reemplazando la escritura manual de
programas. En la presente tesis utilizaré esta técnica garantizando la seguridad por cons-
trucción, la especificación de objetivos de progreso a través de fórmulas fltl sobre dominios
falibles y laadaptabilidad a cambios de configuración.
La declaración de las propiedades en la construcción de los controladores es expresada
en una lógica lineal temporal (LTL). Los modelos basados en eventos han sido creado con
éxito en numerosas oportunidades utilizando este subconjunto de lógicas, expresando de
manera eficiente las propiedades que se espera sean satisfecha por el sistema.
Para la construcción del modelo planteado utilizaremos dos tipos de propiedades prin-
cipales, las relacionadas con la seguridad (safety) en las que se espera que una caracterís-
tica valga siempre durante la ejecución del sistema y las propiedades relacionadas con el
progreso (liveness) que especifican, si se cumple un conjunto de presunciones con infinita
frecuencia, debe cumplirse un conjunto de objetivos con infinita frecuencia. A lo largo de la
tesis expondré casos de estudios utilizando un agente construido con tecnología Lego que
efectuará diversas actividades regido por los controladores sintetizados producto de los mo-
delos construidos con la herramienta MTSA.
Los controladores conseguidos con ésta técnica podrían ser adecuados para procesos de
misión crítica donde pueden expresarse en el dominio de las lógicas temporales lineales, que
es descripto con juegos de reactividad generalizada con propiedades de seguridad (SGR(1))
sobre dominios falibles.
Como parte del desarrollo y mejora de los sistemas, los cambios de configuración son re-
queridos constantemente y al mantenerse de manera declarativa las especificaciones de los
controladores, la técnica de producción automática de programas permite realizar los cam-
bios en los controladores sin necesidad de realizar la re codificación de forma manual por
debajo de la especificación garantizando las propiedades expresadas inicialmente. Adicio-
nalmente el refinamiento de las propiedades de progreso y seguridad genera nuevas versio-
nes de controladores que satisfacen estas propiedades siempre y cuando los mismos existan.
El objetivo de esta tesis es demostrar la aplicabilidad de las técnicas mencionadas en un
entorno donde se puede modelar con el robot Lego Mindstorm NXT y EV3, con sus ventajas
en la construcción de agentes utilizando este tipo de robots y donde el mismo desarrollará
su misión en un ambiente determinado como por ejemplo un edificio, industria, casa, etc.
Para esto el agente transitará por un ambiente construido con caminos e intersecciones.
Demostraré como se puede reconfigurar los modelos para que el agente pueda evitar de-
terminados caminos o solicitar que se asegure transitar otros. Así mismo demostraré cómo
puede el modelo interactuar con otros agentes o con mecanismos de reposicionamiento, todo
esto con la habilidad de reconfiguración prácticamente automática mediante la generación
sistemática de controladores basados en el proceso de síntesis evitando incurrir en la re
1
1. Introducción 2
escritura manual de los mismos.
2. MOTIVACIÓN
2.1. Controladores LTS
Los controladores creados a través de la síntesis de modelos basados en juegos del tipo
SGR(1) poseen un comportamiento que puede expresarse con una máquina de estados con
transiciones etiquetadas, donde el conjunto de transiciones se puede dividir en aquellas que
son controlables como son las operaciones o comandos que se envían al robot, y las transi-
ciones no controlables como son las señales que se reciben de sensores del robot.
A medida que el controlador transita su ejecución es necesario que el mismo no ingrese
en estados indeseables. Asegurar que cualquier interacción del controlador con su ambien-
te o agentes externos no permita estados indeseados requiere de un análisis profundo en
muchos casos analizando las situaciones de error, corrigiéndolos y poniéndolos a prueba
aunque sin asegurar que los mismos se vean resueltos en su totalidad. Esta situación se
torna aún más crítica si de la ejecución del controlador dependen vidas humanas.
Adicionalmente el cambio de requerimientos o aspecto de alguna de las condiciones es-
tablecidas pueden provocar un re-trabajo en la construcción del controlador teniendo que
volver a analizar y re construir corriendo el riesgo de incorporar nuevos fallos al controla-
dor.
Analizaré mediante los casos de estudio cómo la herramienta MTSA permite especi-
ficar objetivos de progreso y condiciones de seguridad de forma que la síntesis produzca
controladores correctos por definición. Mostraré como estos controladores pueden aplicarse
directamente en la robótica utilizando como ejemplo robots Lego NXT y EV3 a través de la
plataforma de integración “Enactments”. Adicionalmente mostraré como los cambios de en-
torno y re definición del modelo puede ser aplicables automáticamente a la re configuración
del controlador cambiando rápidamente el comportamiento del robot.
2.2. Soporte Enactment
En este trabajo se describirá la extensión desarrollada al entorno de modelado MTSA
para que la misma permita la ejecución de controladores sintetizados y que los mismas se
puedan comunicar con diversos dispositivos. A lo largo de la tesis mostrare los detalles en
la construcción de la extensión, como se incorporan nuevos dispositivos externos a la herra-
mienta y el ambiente de ejecución de controladores dentro de la herramienta MTSA.
2.3. Presentación de los casos de estudio
Los casos de estudios presentados desarrollan modelos que inician desde un compor-
tamiento simple del agente sobre un ambiente específico y luego aplicaré cambios en la
configuración del mismo para generar ambientes más sofisticados generando controladores
3
2. Motivación 4
que respondan a las especificaciones dadas. Estos casos de estudios se basarán en activida-
des que realizará el agente construido quien se desplazará a través de un mapa que simula
una configuración de un ambiente determinado, realizando sus acciones según los compor-
tamientos especificados en cada caso. Describiré en los modelos presentados la construcción
del modelo y los resultados obtenidos.
2.4. Resumen de contribuciones
La principal contribución de esta tesis es mostrar cómo es posible construir controlado-
res mediante la síntesis de modelos LTS, poniendo a prueba los mismos en robots y cómo
los cambios en alguno de los aspectos del modelo permiten la generación de nuevos contro-
ladores de forma automática. Para esto se incluye en las contribuciones de este trabajo el
desarrollo del soporte para los robots Lego NXT y EV3 donde los mismos incluye los contro-
ladores de bajo nivel, comunicación junto con el análisis de performance y confiabilidad.
Así mismo este trabajo incluye el co-desarrollo de la extensión Enactment a la herra-
mienta MTSA que sirve como plataforma de ejecución y comunicación entre los controlado-
res sintetizados y dispositivos externos.
Los casos de estudios presentados pondrán a prueba los controladores sintetizados en un
ambiente de ejecución donde permitirán evaluar su comportamiento observando el desem-
peño del robot cumpliendo las actividades deseadas y planteando como los cambios de con-
figuración las características modeladas pueden ser soportadas por la técnica de síntesis
permitiendo la generación automática de nuevos controladores evaluando esta característi-
ca deseable.
2.5. Estructura de la tesis
La presente tesis contiene la siguiente estructura. En principio se darán las prelimi-
nares y fundamentos teóricos. Luego se describirá la extensión “Enactment” desarrollada
para la herramienta MTSA. Para poder validar los trabajos realizados se describirá deta-
lladamente la construcción de un robot basado en Lego NXT, donde se incluirá los esfuerzos
realizados en distintas áreas de la robótica.
3. FUNDAMENTOS
3.1. El Mundo y la Máquina
Comenzamos por ofrecer nociones acerca de la visión general de la ingeniería de reque-
rimientos. En particular, presento el punto de vista de ingeniería de requerimientos de Zave
y Jackson [Jac95a, Jac95b, ZJ97] y de Letier y Van Lamsweerde [vLL00, Lam01]. Ambos
puntos de vista están de acuerdo en que la distinción entrelos problemas del Mundo y la so-
lución de Máquina es fundamental para comprender si la máquina resuelve correctamente
el problema en cuestión. De hecho, el efecto de la máquina en el mundo y las suposiciones
que hacemos acerca de este mundo son fundamentales para el proceso de toma de requeri-
mientos. El problema define una parte del mundo real que queremos mejorar mediante la
construcción de una máquina. Por lo general, incluye algunos de los componentes que inter-
actúan con el mundo siguiendo normas y procesos conocidos. Por ejemplo, una herramienta
de perforación, un brazo de robot o las reglas para el procesamiento de productos que entran
en una línea de producción (véase la Figura 3.1).
Por otra parte, se espera que la solución de la máquina pueda resolver el problema.
Por ejemplo, el ejemplo de la Figura 3.1 muestra que la célula de producción debe iniciar el
procesamiento de los productos, solo si están disponibles en la bandeja de entrada. De hecho,
la sentencia inTray[p]→ get.InTray[p] muestra que se espera que el brazo del robot debe
recoger los productos de la bandeja en el caso de que estén listos para ser procesados. Por
último, los fenómenos compartidos son una parte común entre el problema mundo y la
solución máquina. Por lo tanto, define la interfaz donde la máquina interactúa con el mundo,
representada como la intersección de los dos conjuntos en la Figura 3.1. La máquina se hace
referencia en el contexto de síntesis como el controlador, se utilizará uno u otro término en
función del contexto Podemos referirnos al problema mundo como el modelo de entorno.
Fig. 3.1: World and Machine Phenomena
Las sentencias que describen los fenómenos, tanto del mundo y como la máquina puede
variar en alcance y forma [Jac95a, PM95]. Las sentencias pueden ser en modo indicativo u
optativo [optative mood]. En [vL09], las sentencias que describen el sistema se caracterizan
por ser descriptivas y prescriptivas.
Sentencias descriptivas representan propiedades sobre el sistema que son independien-
tes de cómo se comporta el sistema. Las sentencias descriptivas están en modo indicativo.
5
3. Fundamentos 6
Las sentencias prescriptivas afirman propiedades deseables que pueden estar presentes
o no. De hecho, las sentencias prescriptivas deben ser aplicadas por los componentes del
sistema. Naturalmente, las declaraciones prescriptivas pueden cambiar, fortaleciéndose /
debilitándose o incluso eliminadas mientras que no se puede tornar descriptivas.
Como se mencionó anteriormente, los estados pueden variar en su alcance. Tanto las
sentencias prescriptivas como también descriptivas pueden referirse a características de la
máquina que no son compartidas con el mundo. Otras sentencias pueden referirse a fenóme-
nos compartidos por la máquina y el mundo. Más precisamente, una propiedad de dominio
es una sentencia descriptiva sobre el problema mundo. Estas se deben tener independien-
temente del comportamiento del sistema. En este trabajo llamamos Modelo Ambiente, al
conjunto de propiedades de dominio para un problema particular.
Un supuesto de ambiente es una sentencia que podría no suceder [may not hold] y debe
ser satisfecha por el ambiente. Un requisito de software, o Requisito para abreviar, es una
sentencia prescriptiva a ser aplicadas por la máquina, independientemente de cómo se com-
porta el problema mundo y deben ser formuladas en términos de los fenómenos compartidos
entre la máquina y problema mundo.
Siguiendo [vLL00, Lam01] decimos que una acción es supervisada / controlable si tal
acción es supervisada / controlable por la máquina. Podemos referirnos a acciones supervi-
sadas como acciones no controlables, ya que están controlados por el ambiente.
3.2. Sistemas de Transición Etiquetados
Vamos a describir y fijar una notación para los sistemas de transición etiquetados o La-
beled Transition Systems (LTS) [Kel76], que son ampliamente utilizados para el modelado
y análisis del comportamiento de los sistemas concurrentes y distribuidos. LTS es un siste-
ma de transición de estados donde las transiciones se etiquetan con acciones. El conjunto
de las acciones de un LTS se llama su alfabeto para la comunicación y las interacciones que
el sistema modelado puede tener con su entorno.
Definición (Sistema de Transición Etiquetado) [Kel76]) Sea States un conjunto universal
de estados, Act un conjunto universal de etiquetas. Un Sistema de Transición Etiquetado
(LTS) es una tupla E = (SE, AE,∆E, sE0), donde SE ⊆ States es un conjunto finito de estados,
AE ⊆ Act es un alfabeto finito, ∆E ⊆ (SE × AE ×SE) es una relación, y s0∈SE es el estado
inicial.
Dado (s,`, s′) ∈ ∆E decimos que ` esta activo desde s en E. Decimos que un LTS E es
determinístico si (s,`, s′) y (s,`, s′′) estan en ∆E implica que s′ = s′′. Para un estado s deno-
tamos ∆E(s) = {` | (s,`, s′) ∈ ∆E}. Dado un LTS E, podríamos referirnos a su alfabeto como
αE.
Definición (Composición en Paralelo) Sea M = (SM , AM , ∆M , sM0) y E = (SE, AE,∆E,
sE0) LTSs. Una Composición en Paralelo ‖ es un operador simétrico que E‖M es el LTS
E‖M = (SE ×SM , AE ∪ AM , ∆, (sE0 , sM0)), donde ∆ es la relación mas pequeña que satisface
las siguientes reglas, donde ` ∈ AE ∪ eAM :
(s,`,s′)∈∆E
((s,t),`,(s′,t))∈∆ `∈AE\AM
(t,`,t′)∈∆M
((s,t),`,(s,t′))∈∆ `∈AM\AE
(s,`,s′)∈∆E , (t,`,t′)∈∆M
((s,t),`,(s′,t′))∈∆ `∈AE∩AM
3. Fundamentos 7
Definición (LTS Legal) Dado E = (SE, AE,∆E, sE0), M = (SM , AM ,∆M , sM0) LTSs, y AEu ∈
AE. Decimos que M es un LTS Legal para E con respecto a AEu , si para todos (sE, sM) ∈ E‖M
sucede lo siguiente: ∆E‖M((sE, sM))∩ AEu =∆E(sE)∩ AEu
Intuitivamente, un LTS M es una LTS Legal para y LTS E con respecto a AEu , si pa-
ra todos los estados en la composicón (sE, sM) ∈ SE‖M los contiene, una acción ` ∈ AEu es
deshabilitada en (sE, sM) si y solo si esta esta también deshabilitada en sE ∈ E. En otras
palabras, M no restringe E con respecto a AEu .
Definición (Trazas) Considere un LTS E = (S, A,∆, s0). Una secuencia π= `0,`1, . . . es una
traza en E si existe una secuencia s0,`0, s1,`1, . . ., donde para todo i tenemos (si,`i, si+1) ∈∆.
Definición (Estados Alcanzables) Considere un LTS E = (SE, AE,∆E, s0). Un estado s ∈ SE
es alcanzable (desde el estado inicial) en E si existe una secuencia s0,`0, s1,`1, . . ., donde
para cada i tenemos (si,`i, si+1) ∈ ∆ y s = si+1. Nos referimos a el conjunto de todos los
estados alcanzables en E como Reach(E).
A traves de esta tesis vamos a limitar la atención a aquellos LTSs E donde todos sus
estados s ∈ SE, s son alcanzables.
3.3. Lógica Lineal Temporal de Flujos (Fluent Linear Temporal Logic)
Lógica lineal temporal (LTL) es ampliamente usada para describir el comportamiento de
requerimientos [GM03, vLL00, LvL02, KPR04]. La motivación para escoger un LTL de flu-
jos es que este provee un framework uniforme para especificar propiedades basada en esta-
dos en modelos basados en eventos [GM03]. Fluent Linear Temporal Logic (FLTL) [GM03]
es una lógica linear-time temporal para razonar acerca de flujos. Un flujo Fl es definido por
un par de conjuntos y un valor Booleano: Fl= 〈IFl,TFl,InitFl〉, donde IFl ⊆ Act es el conjunto
de acciones iniciadoras , TFl ⊆ Act es el conjunto de acciones finalizadoras y IFl ∩TFl = ;.
Un flujo puede ser inicializado con trueo f alseindicado por InitFl. Toda acción ` ∈ Act in-
duce un flujo, a saber ˙̀= 〈`, Act \{` } ,false〉. Finalmente, el alfabeto de un flujo es la unión
de sus acciones iniciadoras y finalizadoras.
Sea F el conjunto de todas los posibles flujos sobre Act. Una fórmula FLTL es defini-
da inductivamente usando los conectores Booleanos estándards y operadores temporales
X (next), U (strong until) de la siguiente manera:
ϕ ::=Fl | ¬ϕ |ϕ∨ψ |Xϕ |ϕUψ,
donde Fl ∈F . Introduciremos ∧, F (eventually), y G (always) como una comodidad sintácti-
ca. Sea Π el conjunto de trazas infinitas sobre Act. La traza π = `0,`1, . . . satisface un flujo
Fl en la posición i, denotado como π, i |= Fl, si y solo si uno de las siguientes condiciones es
válida:
InitFl ∧ (∀ j∈N ·0≤ j ≤ i → ` j ∉ TFl)
∃ j ∈N · ( j ≤ i∧` j ∈ IFl)∧ (∀k ∈N · j < k ≤ i → `k ∉ TFl)
Dada una traza infinita π, la fórmula que satisface ϕ en la posición i, denotada como
π, i |= ϕ, es definida como se muestra en la Figura 3.2. Decimos que ϕ se cumple en π,
denotado como π |= ϕ, si π,0 |= ϕ. Una fórmula ϕ ∈ FLTL es cierta si un LTS E (denotado
como E |=ϕ) si éste es cierto en toda traza infinita producida por E.
3. Fundamentos 8
π, i |=Fl , π, i |=Fl
π, i |= ¬ϕ , ¬(π, i |=ϕ)
π, i |=ϕ∨ψ , (π, i |=ϕ)∨ (π, i |=ψ)
π, i |=Xϕ , π,1 |=ϕ
π, i |=ϕUψ , ∃ j ≥ i ·π, j |=ψ∧∀ i ≤ k < j ·π,k |=ϕ
Fig. 3.2: Semántica para el operador de satisfacción
3.4. Problemas de control
El problema de síntesis de control consiste en producir automáticamente una máquina
que restringe la ocurrencia de eventos controlados basada en la observación de eventos que
han ocurrido. Cuando se despliega en un entorno apropiado esta máquina asegura la sa-
tisfacción del conjunto de objetivos de sistema provistos. La satisfacción de estos objetivos
depende de la satisfacción de las presunciones por parte del entorno. En otras palabras,
damos una descripción del entorno, presunciones, objetivos de sistema y un conjunto de ac-
ciones controlables.
Una solución para el problema de control basado en eventos es encontrar una máquina cu-
yo comportamiento concurrente al entorno que satisfaciendo las presunciones satisface los
objetivos.
Definimos el problema de síntesis de control para modelos basados en eventos de la si-
guiente forma: Dada una LTS que describe el comportamiento del entorno, un conjunto de
acciones controlables, un conjunto de fórmulas FLTL para las presunciones del ambiente
y un conjunto de fórmulas FLTL para los objetivos de sistema, el problema de control LTS
consiste en encontrar una LTS que restringe sólo la ocurrencia de acciones controlables y
garantiza que la composición paralela del ambiente con dicha LTS estará libre de deadlocks
y que, si las presunciones de ambiente son satisfecha, satisfacerá también los objetivos de
sistema.
Definición (Control LTS) Dada una especificación de un entorno en forma de una LTS E,
un conjunto de acciones controlables Ac y un conjunto H de pares (Asi,G i) donde Asi y G i
son fórmulas FLTL especificando presunciones y objetivos respectivamente, la solución al
problema de control LTS ε=< E,H, Ac > consiste en encontrar una LTS M de forma que M
sobre el conjunto de acciones controlables Ac y el conjunto de acciones no controlables Ac es
un entorno legal para E, E‖M se encuentra libre de deadlocks, y para cada par (Asi,G i ∈ H)
y para cada traza π en E‖M se cumple que si π |= Asi entonces π |=G i.
Ahora definimos el problema de control SGR(1) que es computable en tiempo polinomial.
Tiene base en los problemas GR(1) y de seguridad pero en un contexto de modelado basado
en eventos. Requerimos que el modelo del entorno E sea una LTS determinística para ase-
gurar que el controlador observación completa del estado del entorno. Requerimos que H
sea (;, I), (As,G) donde I es un invariante de seguridad de la forma äρ las presunciones As
son una conjunción de subfórmulas FLTL de la forma ä♦φ, el objetivo G es una conjunción
de subfórmulas FLTL de la forma ä♦γ y ρ, φ y γ son una combinación booleana de Flujos.
3. Fundamentos 9
Definición (Control LTS SGR(1)) Un problema de control LTS ε =< E,H, Ac > es SGR(1)
si E es determinístico y H = (;, I), (As,G) donde I = äρ, As = ∧ni=1ä♦φi,G = ∧mj=1ä♦γ j, y
ρ, φ y γ son una combinación booleana de Flujos.
3.5. Dominios falibles
Consideramos una técnica que permite la síntesis de controladores aún en entornos que
exhiben fallas. Esta técnica toma el nombre de síntesis con fallas. Por lo general no puede
controlarse a un entorno malicioso para conseguir los objetivos de sistema. De todas formas,
proponemos nociones realistas de equidad que permiten a los controladores comportarse de
la forma esperada por ejemplo para el caso en el que deberían intentar repetir una acción
hasta conseguir una respuesta exitosa.
Distinguimos a las fallas de otras acciones de la siguiente manera, para cada problema de
control definimos un conjunto de triplas try− response (prueba, respuesta), una tripla de
ésta característica captura la relación entre acciones controlables y sus reacciones de éxito
o fracaso. Se precisa que 1) la acción "try"sea controlable, 2) todas las acciones pertenecien-
tes a una tripla try− response sean únicas con respecto a otras triplas del conjunto, 3) un
reintento no ocurra antes de una respuesta 4)las respuestas ocurran solamente como resul-
tado de un intento, 5)existe como máximo una respuesta por cada intento y 6) la decisión de
fallar o tener éxito no sea forzada por otras acciones, con lo que la falla está habilitada sí y
sólo sí el éxito está habilitado.
Definición (Try-Response) Dada una LTS M = (SM ,LM ,∆M , sM0) donde LC ⊆ LM , decimos
que un conjunto T = (tryi, suci, f ail i) es un conjunto try− response para M si se cumplen
las siguientes condiciones para todo i:
1. tryi ⊆ LC, suci, f ail i ∈ L \ LC y suci 6= f ail i
2. Para todo j 6= i, tryi, suci, f ail i ∩ tryi, suci, f ail i =;
3. ¬( ˙f ail i ∨ ˙suci)W ˙tryi
4. ä( ˙tryi ⇒©(¬ ˙tryiW( ˙f ail i ∨ ˙suci)))
5. ä(( ˙f ail i)∨ ˙suci)⇒©(¬( ˙f ail i ∨ ˙suciW ˙tryi))
6. Para todo s ∈ SM , f ail i está habilitado para s sí y sólo sí suci está habilitado para s
La técnica presentada demanda una noción de equidad más fuerte, que describa la pre-
sunción de que si se ejecuta un intento con infinita frecuencia se debe conseguir un éxito
con infinita frecuencia. Esta noción de equidad reforzada está, de hecho, fuertemente vincu-
lada con la estructura de los modelos del entorno y el controlador. Lo que se precisa es que,
para cada estado global (un estado de E‖M), un tryi sucede con infinita frecuencia, f ail i
no sucede con infinita frecuencia. Una forma más intuitiva de expresarlo sería pensar que
la decisión de fallar es equitativa e independiente del estado del controlador o el entorno.
La siguiente definicón captura esta noción de equidad reforzada. Requiere que para cada
transición etiquetada con un try, si es tomada con infinita frecuencia luego success sucede
con infinita frecuencia antes del próximo try.
3. Fundamentos 10
Definición (t-strong fairness) Dada una LTS M y un try-response T para M, una tra-
za π ∈ tr(M) es t-strong fair (fuertemente t-equitativa) con respecto a M y T si para todo
(tryi, suci, f ail i) ∈ T y para todas las transiciones t = (s, tryi, s′) vale que: π′ |= ä♦try′i ⇒
ä♦(¬tryiUsuci), donde π′ = ε′|LM∪{trybi }, ε
′ = ε|[s.tryi .sb/s.tryi .trybi ,sb], y ε es una ejecución de
M tal que ε′|LM =π.
Cabe notarse que w|A es la proyección de la palabra w sobre el alfabeto A y que w[v/vb]
es el resultado de reemplazar en w todas las ocurrencias de v con vb.
Hace falta extender la noción de equidad aún más para cumplir la noción intuitiva de
que las presunciones del entorno deben ser independientes de las fallas, particularmente
porque la elección de una falla o de un éxito puede entenderse como no-determinística dado
que abstrae la verdadera causa del éxito o fracaso.
Formalizamos esta noción de la siguiente forma, restringimos las trazas de interés a aque-
llas que satisfacen que las presunciones deben poder cumplirse con infinita frecuencia sin
observar fallas, o, más precisamente, que si el controlador intenta con suficiente frecuencia,
entonces no sólo tendrá éxito, sino que tendrá éxito a la vez que satisface todas las pre-
sunciones. Esto es, que si las presunciones y las fallas son verdaderamente independientes,
intentar la acción con suficiente frecuencia garantiza que en algún punto luego de un inten-
to, ninguna falla sucederá en tanto no se hayan satisfecho todas las presunciones.
Definición (Strong Independent Fairness) Dada una LTS M y un try-response T para M y
A un conjunto de fórmulas FLTL, una traza π ∈ tr(M) se dice Strong Independent Fair (de
equidad reforzada independiente) respecto de A si para todo (tryi, suci, f ail i) ∈ T y parato-
da transición t = (s, tryi, s′) vale que π |=ä♦try′i ⇒ä♦((¬tryiUsuci)∧(
∧n
i=1(¬(
∨n
j=1 f ail j)W A i))),
donde π′ = ε′|LM∪trybi ,ε
′ = ε|[s.tryi .sb/s.tryi .trybi ,sb], y ε es una ejecución de M tal que ε
′|LM =π.
Formalizamos a continuación el problema de control bajo las condiciones de equidad
arriba presentadas. Toma el nombre de problema de control con éxito recurrente (recurrent
success control problem). Para todas las trazas que sean de equidad reforzada independien-
te garantiza propiedades generales de seguridad y progreso que son del tipo GR(1). Exten-
demos el problema de control SGR(1) definido en 3.4 introduciendo fallas y expectativas
sobre la equidad del ambiente.
Definición (Recurrent Success) Dado un problema de control SGR(1) LTS L =< E,H,Lc >
y un try-response T para L , la solución del problema de control de éxito recurrente R =<
L ,T > consiste en encontrar un LTS M tal que M con acciones controlables Lc y no controla-
bles Lc es un entorno legal para E, E‖M no contiene deadlocks y para cada par (Asi,G i) ∈ H,
para cada (tryi, suci, f ail i) y para cada traza de equidad reforzada independiente π en M‖E
vale que si π |= Asi entonces π |=G i.
3.6. Procesos de Estados Finitos (FSP)
Hasta ahora, hemos descripto LTSs (MTSs) definiendo sus componentes, ej. estados,
acciones, relaciones de transición (requeridos y posibles), y el estado inicial. Esta represen-
tación es válida para LTSs (MTSs) con pocos estados. Sin embargo, esta representación se
torna impráctica cuando trabajamos con LTSs (MTSs) extensos. Por esta razón, usamos un
3. Fundamentos 11
proceso simple llamado denotado algebra de Procesos de Estados Finitos (FSP) que expeci-
fican textualmente un LTSs [MKG97, MK06].
FSP es una especificación de lenguaje con una bien definida semántica en términos de
LTSs (MTSs), que provee de manera concisa una forma de describir un LTSs. Cada expre-
sión FSP E puede ser mapeada en un LTS (MTS) finito, usaremos lts(E) para denotar el
LTS (MTS) que le corresponde. A continuación discutiremos brevemente la sintaxis FSP.
Como un ejemplo, en la Figura 3.3, mostramos el código FSP de un proceso de cocción
de cerámica.
En FSP, los nombres de procesos comienzan con mayúsculas y las acciones comienzan
con minúscula. El código para la cocción de cerámica define 2 procesos FSP, uno mode-
la el proceso que simplemente esta en espera, llamado f sp(IDLE), y otro proceso llamado
f sp(DOMAIN). Adicionalmente, f sp(DOMAIN) define los procesos auxiliares f sp(COOK ING),
f sp(COOKED), y f sp(OH). Los procesos auxiliares son locales para el proceso FSP de la
forma que han sido definidos. f sp(DOMAIN) es definido usando la acción y el operador
f sp(−>) junto a la recursión. Por ejemplo, el proceso se encuentra definido para comenzar
ejecutando indistintamente f sp(idle) quedándose en este o f sp(cook) que comienza con el
proceso de f sp(COOK ING).
Fig. 3.3: FSP Example
FSP soporta numerosos operadores para la composición como la composición en paralelo
de LTS y MTS, o la fusión de MTSs [FDB+10]. El operador para composición en paralelo,
denotado como f sp(||) es definido para preservar la semántica de la composición en pa-
ralelo de LTS presentado en 3.2. Así, dados dos procesos FSP f sp(P) y f sp(Q), tenemos
que: f sp(lts(P||Q)=lts(P)||lts(Q)).
Los procesos FSP processes que son definidos mediante la composición de dos proce-
sos no auxiliares son llamados procesos compuestos y sus nombres contienen el prefijo
f sp(||). Así la composición en paralelo de los procesos FSP f sp(IDLE) y f sp(DOMAIN) es
f sp(||IDLEDOMAIN = (IDLE||DOMAIN)).
Finalmente, un FSP posee un número de palabras reservadas que son usadas antes
de la definición de un proceso y estas forzan al MTSA a desarrollas operciones comple-
jas sobre el proceso. Por ejemplo, el comando, f sp(minimal), indica que MTSA construya
el LTS/MTS minimal respetando fuertemente la semántica equivalente y la instrucción,
f sp(deterministic), instruye para que MTSA construya el LTS minimal con respecto a su
traza.
También el FSP permite definir propiedades FLTL. Un flujo que marca aquellos esta-
dos donde la cerámica es cocinada puede ser expresado en FSP con el siguiente código:
f sp( f luentCooking =< cook, f inishedCooking > initiall y0). f sp(Cooking) se encuen-
tra inicialmente en falso, este se torna verdadero con f sp(cook) y este se torna falso nueva-
mente cuando ocurre f sp( f inishedCooking).
3. Fundamentos 12
Sumarizando, FSP provee el soporte requerido para especificar LTSs and FLTL formu-
las. Dicho soporte es requerido para expresar el modelado del entorno y los objetivos del
controlador.
4. HERRAMIENTA MTSA
MTSA (Modal TRasition System Analyzer) es una herramienta que da soporte a la cons-
trucción, análisis y elaboración de Modal Trasition Systems (MTS) [DFCU08].
Para los propósitos de esta tesis se usará la herramienta para cubrir los siguientes
requerimientos:
Modelado: Creación de los modelos donde se define el comportamiento esperado del robot,
entornos y las propiedades esperadas del sistema. Se utilizará la extensión a la sinta-
xis FSP que permite describir propiedades como fórmulas FLTL y controladores como
un conjunto de propiedades de progreso, seguridad, acciones falibles, controlables y
no controlables
Síntesis: Creación de controladores sintetizados a partir de las propiedades especificadas
componiendo con el entorno permitiendo que el controlador satisfaga los objetivos de
progreso y seguridad
Ejecución: Ambiente donde pondremos en ejecución el controlador sintetizado que contro-
lará e interactuará con los componentes del sistema configurados
4.1. Construcción
La herramienta MTSA permite describir modelos se a través de una extensión del len-
guaje de Procesos de Estados Finitos (FSP). FSP es un lenguaje centrado en la construcción
por composición de modelos complejos.
FSP incluye varios operadores tradicionales para describir modelos de comportamiento,
como puede ser el prefijo de acción (−>), elección (|),composición secuencial (;), composición
paralela (||) y mezcla.
La semántica de composición permite que dadas dos descripciones parciales del mismo
componente, el operador de composición devuelve una MTS que combina la información
provista por las descripciones parciales originales. Aun cuando los operadores composicio-
nales permiten la construcción de MTS complejas, construir los modelos a ser compuestos
sigue siendo una tarea dificultosa de intenso trabajo que requiere un grado considerable de
experiencia. Con el fin de facilitar esta tarea, MTSA provee la funcionalidad que permite
sintetizar modelos de comportamiento de forma automática a partir de las especificaciones
declarativas de los requerimientos, escenarios y casos de uso.
La palabra clave constraint de MTSA se usa en conjunción con las propiedades de se-
guridad (safety) formalizadas haciendo uso de Lógica Lineal Temporal de Flujos (FLTL).
Para una declaración de tipo constraint MTSA construye automáticamente el modelo de
MTS que caracteriza a todos los modelos LTS libres de deadlock que satisfacen la fórmula
FLTL. Al sintetizar y mezclar los modelos MTS obtenidos con definiciones FLTL, se puede
construir de forma iterativa una MTS que caracteriza a la cota superior de los sistemas de
13
4. Herramienta MTSA 14
comportamiento esperados.
La palabra clave abstract de MTSA puede aplicarse a procesos FSP. Su semántica es
tal que el modelo resultante es la MTS de menor refinamiento que garantiza el comporta-
miento requerido por los procesos FSP. Esta palabra clave, utilizada en conjunción con los
procesos FSP que modelan el comportamiento descripto en la especificación del escenario,
provee una MTS que caracteriza a todas las implementaciones que satisfacen dicha especi-
ficación (i.e. la cota inferior del comportamiento esperado del sistema).
4.2. Análisis
Luego de las actividades de modelado del sistema, el análisis pasa a ser una actividad
importante que puede brindar información relevante acerca del dominio del problemacomo
de la solución. Esto permite poder validar si las características modeladas son acordes a al
problema a modelar.
La herramienta brinda soporte a varios tipos de análisis, comenzando por la inspección
de modelos MTS y a través de la construcción automática de representaciones visuales de
los modelos MTS escritos usando FSP. La inspección queda sujeta al tamaño del modelo,
esta limitación puede mitigarse haciendo uso de los operadores de minimización y oculta-
miento.
Si bien la inspección y animación no permiten una exploración exhaustiva de los mo-
delos MTS, MTSA implementa un número de técnicas de análisis automáticas para éste
propósito. En particular, MTSA permite verificar si un modelo MTS satisface una propie-
dad expresada en FLTL. Un modelo MTS caracteriza un conjunto de implementaciones, de
las cuales algunas pueden satisfacer la propiedad siendo verificada y algunas pueden vio-
larla.
Mientras que un Modelo MTS M puede caracterizar a un conjunto extremadamente
grande, potencialmente infinito, de implementaciones, verificar una propiedad en M con
model checking se reduce a dos verificaciones tradicionales de FLTL. Finalmente, MTSA
permite verificar si un modelo es libre de deadlocks. Al igual que en el caso de model chec-
king para propiedades FLTL, el resultado de esta verificación tiene uno de tres valores: o
bien todas las implementaciones exhiben deadlocks, o bien todas son libres de deadlock o
bien hay una combinación de implementaciones que exhiben deadlocks y otras que no.
5. MOTIVACIÓN EXTENSIÓN MTSA TOOL
Con el propósito de poder vincular la robótica a ésta herramienta, se ha desarrollado
una extensión llamado “Enactment” que es un framework abierto, extensible y con una API
que permite ejecutar controladores sintetizados brindando interacción con componentes ex-
ternos como por ejemplo robots. En este trabajo se ejecutaran controladores sintetizados a
partir de la especificación que describe un juego SGR(1) sobre dominios falibles.
La habilidad de ejecución de controladores sintetizados o Enactment es una necesidad
a desarrollar aportando nuevos aspectos de conocimiento. Esta nueva extensión ayudará
a observar y monitorear los modelos pudiendo aplicarse tareas de refinamiento sobre las
especificaciones de los controladores construidos, como así también las técnicas empleadas
en su construcción y la forma en que las especificaciones se ajustan los contextos.
Las representaciones de un problema utilizando sintaxis de procesos finitos las realiza-
mos comúnmente mediante un sistema de transiciones etiquetadas. En la sintaxis utilizada
separamos aquellas transiciones controlables de las no controlables. A partir de esto relacio-
namos mensajes de control con las transiciones controlables y con los mensajes de entrada
para un agente. Luego los mensajes de estado se corresponden con las transiciones no con-
trolables en la especificación y mensajes de salida del agente. Por ejemplo como transiciones
controlables o mensajes de control pueden ser comando primitivos para indicar una acción
al agente como ser “mover hacia adelante”, por otro lado un mensaje claro de estado o transi-
ción no controlable puede ser “baja batería” del agente. En esta tesis trabajare con modelos
en los cuales de todo estado saldrán o todas transiciones controlables o todas no controlables
evitando estados donde existe una combinación entre ambos tipos de transiciones. En un es-
tado particular, no controlable, podría suceder que exista más de una transición de salida,
una representando un mensaje de estado, otra representando un mensaje de timeout para
expresar la posibilidad de que una máquina no responda en un lapso razonable de tiempo.
C U
control
status
C U
request
timeout
C U
request
repl y
timeout
Fig. 5.1: Transición entre estados controlables y no controlables: control-estado (izq.),
request-timeout (centro), request-timeout,reply(der.)
Un subconjunto de las transiciones no controlables está relacionado al modelo de fa-
llas, indicando estados en los cuales una transición puede suceder pero con cierta noción de
equidad. Estas transiciones del modelo de falla deben capturar un comportamiento no sis-
temático, independiente entre sí que va a dar lugar (eventualmente) a la ejecución de otra
transición en ese mismo estado. La tripla (try, success, fail) permite representar la na-
turaleza falible pero no sistemática del robot como por ejemplo (r1.turnRight, r1.sucess,
r1.lost).
15
5. Motivación Extensión MTSA Tool 16
5.1. Arquitectura
El módulo MTSA Enactment ha sido diseñado con el fin de poder cubrir las necesidades
de extensibilidad, flexibilidad y ejecución de modelos. La arquitectura propuesta permite la
incorporación de nuevas extensiones a la herramienta mediante la implementación y regis-
tros de Enactors. Los Enactors son las unidades funcionales del entorno de simulación. Las
mismas interactúan entre sí y con el ambiente mediante eventos/suscriptores. Las simula-
ciones son orquestadas por un Scheduler determinado. El mismo es una especialización de
Enactor y es el responsable de escoger las acciones disponibles regidas por el controlador
basado en una política determinada. Las simulaciones son ejecutadas en la herramienta
con un entorno especialmente diseñado donde puede el usuario puede darle seguimiento
mediante una interfaz gráfica.
5.2. Enactors
Dentro del entorno de ejecución de controladores sintetizados o “Enactment” definimos
como Enactor a todo agente activo con capacidades de interacción con sus pares escuchan-
do y emitiendo eventos. El componente de ejecución respeta un esquema de comunicación
asíncrona y con un grado de abstracción suficiente para permitir controlar y monitorear los
distintos agentes del entorno. Se puede pensar que cada Enactor expone una API. Los méto-
dos públicos son equivalentes a los mensajes de control y los eventos disponibles equivalen
a los mensajes de estado. Puede suceder que el vínculo entre un mensaje en el dominio de
control discreto y su contraparte en el dominio real oculte información. En esta tesis se
implementará una relación directa entre las transiciones controlables como mensajes de
control y estos tendrán su equivalente a primitivas que se enviarán mediante un canal de
comunicación inalámbrica al agente quien ejecutará la instrucción. Cada vez que la interfaz
de comunicación recibe un mensaje proveniente del robot, el adaptador (enactor) lo interpre-
ta y produce un evento que contiene información relacionada a la transición no controlable
(mensaje de estado).
En la figura 5.2 se representa la relación entre el modelo utilizado para construir la
especificación del controlador y su implementación. C representa a los estados controlables
en el modelo y U representa a los no controlables. c representa a la implementación del con-
trolador en el entorno de ejecución y a representa al enactor en calidad de adaptador entre
los mensajes del entorno de ejecución y los del dominio del componente (potencialmente)
externo al entorno de ejecución. Se ve como las transiciones en el modelo se corresponden
con los mensajes de control y estado en el entorno de ejecución.
5. Motivación Extensión MTSA Tool 17
C U
c a
enact enact
controllable
non− controllable
control
status
Fig. 5.2: Relación de ejecución entre el modelo y los componentes de ejecución
La relación entre la implementación en la tecnología correspondiente y el modelo se
muestra en la figura 5.3 representando al componente de ejecución como e para indicar que
se está hablando de un objeto Enactor que se ejecuta dentro de la herramienta. Según la
arquitectura escogida las transiciones controlables y no controlables se relacionan con lla-
madas a función y eventos respectivamente.
C U
c e
enact enact
controllable
non− controllable
APIcall
event
Fig. 5.3: Relación de ejecución entre el modelo y la implementación final de los componentes
de ejecución
Por otro lado buscando la expansión en la interacción de un Enactor con un agente como
muestrala figura 5.4, se plantea el siguiente esquema arquitectónico en el cual se cuenta
con un robot Lego Mindstorm NXT o EV3 (representado por r) donde el Enactor e que resi-
de dentro del entorno de ejecución de la herramienta se comunica con el agente r enviando
mensajes de control a través del canal de comunicación inalámbrico (Bluetooth) y el mismo
envía de regreso mensaje de estado que son interpretados como eventos por parte del Enac-
tor e.
Dentro de los modelos que trabajan con técnicas de control continuo, se puede plantear
dentro de la relación de los modelos basados en eventos y el componente de ejecución, la
ejecución del bloque de control continuo representado con par <control, status>. Este plan-
teo expone la adaptación de este tipo de técnicas de ejecución y otros esquemas de control
en sistemas embebidos que suelen utilizar máquinas de estado finito para representar su
comportamiento como muestra la figura 5.5.
5. Motivación Extensión MTSA Tool 18
Fig. 5.4: Relación Enactor y MTSA
Fig. 5.5: Mensaje control y estado del Enactor
5.3. Controller / Scheduller
Los Controllers o Schedullers son una clase especial de Enactor dentro del entorno de
ejecución de Enactment. Por cada instancia de ejecución existe solo un tipo de Controller.
El mismo es el responsable de implementar la estrategia de selección de las transiciones
controlables. Pensamos en estrategias cuando tenemos situaciones en las cuales desde un
estado controlable especifico parten 2 o más transiciones controlables. Recordamos que en
5. Motivación Extensión MTSA Tool 19
la presente tesis se cubre únicamente los casos en que las de los estados solo parten transi-
ciones controlables o no controlable únicamente.
Un Scheduller especifica alguna estrategia en particular de selección de transiciones
controlables. Como estrategias entendemos por ejemplo seleccionar del conjunto de transi-
ciones controlables una al azar. Otra estrategia puede resumirse como escoger la primera
transición de una lista ordenada bajo algún criterio determinado.
Una vez establecido el Scheduller a utilizar en la ejecución el mismo se encargará de
implementar la estrategia de selección a lo largo de toda la ejecución. Como todo Enactor,
el Scheduller escucha los eventos del entorno emitidos por otros Enactors, y por cada nuevo
estado controlable selecciona del conjunto de transiciones controlables aquella que satisface
las reglas de la estrategia inherente.
5.4. Framework Enactment
Como se ha mencionado anteriormente, la extensión Enactment hace referencia al en-
torno de ejecución para controladores sintetizados que interactúan con los componentes
Enactors. Este entorno es contenido dentro de la extensión co-construida en la presente te-
sis junto al trabajo realizado en [Cer14] que consiste en el componente de simulador de la
herramienta MTSA.
El entorno de simulación consta de las siguientes partes:
El controlador sintetizado producto del modelo LTS
Enactors seleccionados de la lista de componentes registrados mediante la interfaz de
extensión
Scheduller seleccionado para definir la estrategia a seguir
El usuario tiene la habilidad de seleccionar las partes intervinientes en la simulación
ingresando por el menú de MTSA Enactment->Options
Fig. 5.6: Menu Enactment
En la sección de opciones de Enactment (figura 5.7) se despliega la lista de Enactors
registrados como extensión de la herramienta. En la sección 5.5 se describe el mecanismo
de registro de Enactors y Schedullers.
5. Motivación Extensión MTSA Tool 20
Fig. 5.7: Menu Enactment
Una vez que se seleccionan los actores intervinientes en la ejecución del controlador, el
usuario indica el comienzo de la misma mediante la opción ubicada en el menú Enactment-
>Run
Fig. 5.8: Menu Enactment Run
Al comenzar la ejecución se despliega el entorno gráfico de control y monitoreo de la
ejecución. Como se aprecia en la figura el entorno se divide en 3 partes. Sección 1 barra de
herramientas con opciones para pausar y detener la ejecución, controles de visualización del
grafo de progreso. En la sección 2 y principal la herramienta despliega un grafo de progreso
de ejecución. El mismo representa con círculos los estados por los cuales la ejecución recorre
y con arcos las transiciones disponibles. El estado vigente en la ejecución se encuentra colo-
reado de azul y el estado inicial coloreado de gris. En la sección 3 se encuentra la consola de
notificaciones. Aquí se despliega información detallada acerca del avance de la ejecución.
5. Motivación Extensión MTSA Tool 21
Fig. 5.9: Enactment Simulation Windows
Internamente el componente de ejecución MTSAEnacmentSimulation da lugar a la ini-
cialización de los Enactors seleccionados para la instancia de ejecución. Las instancias son
obtenidas a través EnactorFactory del conjunto de Enactors disponibles registrados me-
diante el mecanismo de registro de extensiones utilizando Spring Beans. En 5.5 se describe
en detalle este mecanismo. Cada instancia de Enactor se ejecuta utilizando su propio hilo
de proceso. Una vez obtenidas las instancias de los Enactors, el componente de ejecución
obtiene la instancia del Scheduller escogido de la lista de Schedullers registrados en la he-
rramienta utilizando un mecanismo similar a los Enactors basando en Spring Beans. En
la sección 5.5 se describe en detalle este mecanismo. Obtenida todas las instancias intervi-
nientes, se procede a realizar las subscripciones a eventos entre los Enactors y el Scheduller
como los grafica la figura 5.10.
Fig. 5.10: Scheduller - Enactors subscription
Cuando una ejecución es iniciada, el controlador comienza en su estado inicial y los
Enactors participantes de la ejecución son notificados, en particular el Scheduller quien es
el que escoge la primera acción controlable según la estrategia que este implemente. Una
vez escogida la transición el Scheduller actualiza el estado del controlador y notifica a los
Enactors subscriptos. Cada Enactor escucha los eventos emitidos por el Scheduller y a la
vez pueden emitir eventos relacionado con transiciones no controlables. Al momento de re-
gistrar los enactors, se puede especificar bajo que etiqueta queda establecido cada comando
que el enactor es capaz de reaccionar y bajo qué etiquetas se establece las acciones que el
enactor tiene la habilidad de emitir. Estas etiquetas corresponderán a la definición de las
transiciones controlables y no controlables del controlador sintetizado.
5. Motivación Extensión MTSA Tool 22
5.5. Extensiones – Construcción y registro
La extensión del framework de Enactment puede realizarse mediante la incorporación
de nuevos Enactors o nuevos Schedullers. Los Enactors son aquellos agentes quienes acep-
tarán transiciones controlables y podrán disparar transiciones no controlables al controla-
dor. El desarrollo de nuevas extensiones del framework se realiza mediante la extensión de
clases abstractas y luego el registro en un archivo de configuración xml de la herramienta
MTSA. Dado que el lenguaje escogido para la escritura de la extensión en Java, las exten-
siones deben escribirse en este lenguaje, la menos los componentes que implementan las
interfaces.
Debido a que los mensajes son potencialmente asincrónicos, se ha propuesto utilizar un
esquema basado en eventos. Este esquema nos permite mantener desacoplada la interac-
ción entre los distintos agentes del entorno.
Para esto se presentan 2 clases relacionadas con la recepción de eventos representando
las situaciones en que se reciben mensajes de control y la emisión de eventos representando
el caso en que se envían mensajes de estado. Tendremos un componente de ejecución que
tendrá la composición de estas 2 clases.
public abstract class TransitionDispatcher<Action> {
public synchronized void
addTransitionEventListener(ITransitionEventListener<Action> listener){
...
}
protected void fireTransitionEvent(Action action) throws Exception{
...
}
}
Fig. 5.11: Objecto de emisión de mensajes (TransitionDispatcher)
En la figura 5.11se presenta el resumen de la clase abstracta de emisión de mensajes. La
figura describe el mecanismo de subscripción en la cual un listener que implemente ITran-
sitionEventListener puede registrarse para recibir los mensajes de un enactor mediante
addTransitionEventListener. Debido a que los enactors extiende TransitionDispacher
pueden disparar mediante fireTransitionEvent las acciones a sus subscriptores.
Como se aprecia en la definición, el tipo de dato que define la acción Action es abstraído
siguiendo el patrón de diseño heredado por la construcción de MTSA que no fija que tipo de
dato primitivo es una acción utilizando en este caso “Java Generics”.
5. Motivación Extensión MTSA Tool 23
public interface ITransitionEventListener<Action> {
public void handleTransitionEvent(TransitionEvent<Action>
transitionEvent) throws Exception ;
}
Fig. 5.12: Objecto de recepción de mensajes (ITransitionEventListener)
En la figura 5.12 se describe la interface que define el mecanismo en la cual los imple-
mentadores recibirán los eventos TransitionEvent mediante el llamado al método handle-
TransitionEvent.
La clase abstracta Enactor es la responsable de ser el actor funcional principal de una
simulación dentro del entorno Enactment. La misma extiende a TransitionDispatcher lo
cual significa que otros objetos que implementan ITransitionEventListener podrán subs-
cribirse a sus eventos. También esta clase implementa ITransitionEventListener, lo cual
quiere decir que puede subscribirse a los eventos de otros Enactors. Adicionalmente la clase
implementa Runnable para tener la habilidad de poder ejecutar cada instancia de Enactor
bajo su propio hilo de ejecución. Este diseño permite soportar la comunicación asincrónica
no bloqueante en la interacción del modelo basado en eventos.
public abstract class Enactor<State, Action> extends TransitionDispacher<Action>
implements ITransitionEventListener<Action>, Runnable {
...
}
Fig. 5.13: Clase Enactor (Enactor)
Como se explicó en el capítulo anterior, una clase especial de enactor son los contro-
llers. Los mismos se describe bajo la clase abstracta BaseController quien extiende a
Enactor incorporando funcionalidad de control sobre los estados del controlador sintetiza-
do puesto en ejecución y a su vez ante los eventos que sucede en la ejecución puede tomar
decisiones basado en la estrategia takeNextAction(). Este método es abstracto y es deber
de los implementadores de BaseController dar la especificación a este método definiendo su
comportamiento característico.
5. Motivación Extensión MTSA Tool 24
public abstract class BaseController<State, Action> extends Enactor<State,
Action> {
...
public BaseController(String name, LTS<State, Action> lts, Set<Action>
controllableActions) {
...
}
..
public abstract void takeNextAction() throws Exception;
...
}
Fig. 5.14: BaseController
Las implementaciones de referencias que se proponen inicialmente son TakeFirstCon-
troller quien implementa una estrategia de simplemente tomar la primera acción contro-
lable disponible y RandomController quien se encarga de tomar aleatoriamente la acción
controlable. Cualquier futura estrategia de controlador que se desee incluir en la herramien-
ta debe extender BaseController y registrarse en el archivo de configuración de contexto de
MTSA como se describe más adelante.
Las extensiones de enactors relacionadas a los componentes externos que aceptan como
instrucciones acciones controlables deben extender a la clase abstracta Enactor. La mis-
ma se recomienda que defina en su constructor la definición de las acciones controlables y
no controlables que el Enactor podrá interpretar y enviar como notificación al controlador.
Como se ha mencionado anteriormente no se especifica el tipo de dato que es una acción
y se define en la clase Enactor como un tipo genérico y aquellos enactors concretos deben
respetar este diseño.
En este trabajo se ha implementado el enactor NXTRobot quien implementa la inter-
faz con el robot Lego NXT. Para este trabajo se especificó el siguiente conjunto de coman-
dos o acciones controlables y no controlables: sucess, failure, lost como parte de las no
controlables de estado y follow, turnLeft, turnRight, turnAround y calibrar como las
controlables. Dado el esquema de comunicación propuesto basado en la respuesta bajo un
conjunto de acciones de estado (sucess, failure, lost) se ha definido este comportamiento
bajo un adaptador de robot RobotAdapter el cual extiende a Enactor. El robot Lego NXT
extiende a RobotAdapter asegurando que al menos el conjunto de las acciones no contro-
lables que tendrá serán este conjunto tal como indica el siguiente código.
public class NXTRobot<State, Action> extends RobotAdapter<State, Action> {
...
}
Fig. 5.15: NXTRobot
El enactor NXTRobot como muestra la figura 5.15 recibe en su método primitiveHand-
leTransitionEvent los mensajes de acciones de transición del controlador y los mapea con
5. Motivación Extensión MTSA Tool 25
los follow, turnLeft, turnRight, turnaround asignados y delega la comunicación con el robot
a través de NXTRobotComm. Esta clase que se encuentra en un nivel inferior en el stack
implementado establece la comunicación mediante Bluetooth con el dispositivo basado en
una búsqueda o especificación mediante un identificador proporcionado. Es esta clase la
encargada de codificar los comandos provenientes de NXTRobot y transmitirlos al agente
externo y recibe los estados del robot y notificando a NXTRobot quién este último codifica
en Action y dispara de regreso el evento pertinente de estado al controlador.
Para poder registrar un nuevo enactor que extiende a Enactor en la herramienta MTSA,
es necesario registrar el mismo en el archivo de contexto de configuración ltsa-context.xml.
El mismo se encuentra dentro del classPath de la herramienta. Se debe agregar una sección
xml bean donde se le asigna un “id” único y se hace referencia a la clase que se desea incor-
porar. Luego se mapean las acciones y parámetros de configuración según se especifique en
la firma del constructor de la clase en cuestión.
El siguiente es un ejemplo se puede observar como se incorpora un nuevo enactor con id
nxt1:
<?xml version="1.0" encoding="UTF-8"?>
<beans xmlns="http://www.springframework.org/schema/beans"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xmlns:context="http://www.springframework.org/schema/context"
xsi:schemaLocation="http://www.springframework.org/schema/beans
http://www.springframework.org/schema/beans/spring-beans-3.0.xsd
http://www.springframework.org/schema/context
http://www.springframework.org/schema/context/spring-context-3.0.xsd">
<context:annotation-config/>
<!-- Enactors -->
<bean id="nxt1" class="ar.uba.dc.lafhis.enactment.robot.NXTRobot">
<constructor-arg index="0" value="NXT Robot"/>
<constructor-arg index="1" value="success"/>
<constructor-arg index="2" value="fail"/>
<constructor-arg index="3" value="lost"/>
<constructor-arg index="4" value="follow"/>
<constructor-arg index="5" value="turnLeft"/>
<constructor-arg index="6" value="turnRight"/>
<constructor-arg index="7" value="turnAround"/>
<constructor-arg index="8" value="calibrar"/>
<constructor-arg index="9" value="0016531b6519"/>
<constructor-arg index="10" value=""/>
</bean>
Cabe destacar que pueden haber múltiples instancias del mismo enactor con diferente
id. Con este registro ya puede observarse el enactor en la lista disponible para las simula-
ciones como se muestra en la siguiente figura 5.16:
5. Motivación Extensión MTSA Tool 26
Fig. 5.16: Enactment Options
Para el registro de nuevos controladores que implementan BaseController o derivados
se debe ingresar un nuevo registro “bean” en el archivo de configuración de contexto ltsa-
context.xml donde se especifica su id y la referencia a la clase del nuevo controlador. En el
cuerpo del tag se especifica los parámetros de firma del constructor. En el ejemplo se observa
el registro de los controladores TakeFirstController.
<!--Controller Enviroments / Schedulers-->
<bean id="controllerScheduler"
class="ar.uba.dc.lafhis.enactment.TakeFirstController">
<constructor-arg index="0" value="Take First Controller"/>
</bean>
5.6. Enactors Útiles
Para facilitar las actividades de análisis, seguimiento y depuración de las simulaciones
en el entorno Enactment, se han desarrollado lo siguientes Enactors:”
Counter Enactor enactor que sirve de contador de acciones que transcurren en una simu-
lación. Permite poder llevar estadísticas de ejecución
UI Controller controlador que permite mediante una interfaz gráfica que el usuario pueda
manualmente controlar las acciones que se desarrollan en la simulación. A medida
5. Motivación Extensión MTSA Tool 27
que la simulación transcurre el controlador notifica al usuario las acciones que éste
toma conocimiento y actualiza con las acciones que el usuario tiene disponibles para
continuar con la simulación
6. LEGO MINDSTORM
Lego Mindstorm es un juego de robótica fabricado por la empresa Lego, el cual posee
elementos básicos de las teorías de robótica que permite la construcción de robots de forma
sencilla gracias al ensamblado de las piezas tradicionales de esta firma, sumado a compo-
nentes como motores paso a paso, sensores y una unidad de control programable. Todos los
componentes son fácilmente ensamblables y combinables y los mismos son de una calidad
destacable permitiendo la configuración en tiempo de record sorteando la mayoría de las
problemáticas triviales que la electrónica y robótica presentan.
Al momento de la escritura de esta tesis Lego presenta los modelos RCX, NXT y EV3.
Esta tesis se concentra en el modelo NXT y de forma experimental con el modelo EV3.
6.1. Hardware
El hardware está compuesto por las múltiples piezas de construcción tradicionales de
Lego de las cuales no entraré en detalle y los componentes de robótica que caracterizan a
esta versión.
A continuación una breve descripción del hardware disponible en la versión Lego NXT
Fig. 6.1: Lego Hardware
Unidad de procesamiento Unidad de control programable. La misma es re configu-
rada con una imagen provista por el entorno Lejos el cual permite controlar el hardware
utilizando una API bajo el lenguaje JAVA. Los desarrollos del presente trabajos están cons-
truidos utilizando esta arquitectura abierta.
28
6. Lego Mindstorm 29
Fig. 6.2: Lego Unidad Control
Servomotores Los servomotores no son simples motores, ya que tienen una doble fun-
ción. En primer lugar, podemos hacer que se muevan a una determinada velocidad o con
determinados ángulos, pero además, también pueden actuar como sensores de rotación
Fig. 6.3: Lego Servomotor
Sensor de sonido El sensor de sonido incorpora un pequeño micrófono, permitiendo
así que se pueda programar un robot para que pueda reaccionar ante señales acústicas
Fig. 6.4: Lego Sonido
Sensor de contacto El sensor de contacto incorpora un pequeño pulsador, con lo que,
por ejemplo, se podría crear un pequeño parachoques que detectara si el robot ha impactado
con algo que tiene delante.
6. Lego Mindstorm 30
Fig. 6.5: Lego Contacto
Sensor de distancia El sensor de distancia es capaz de medir distancias de 7 a 1,80
metros, aportando a nuestro robot una capacidad de visión muy interesante. Funciona al
igual que la visión de los murciélagos, a través de ultrasonidos.
Fig. 6.6: Lego Distancia
Sensor de color El sensor de color es capaz de distinguir 3 niveles de colores (RGB), es
decir, rojo, verde, y azul. Este sensor es utilizado en el presente trabajo para el seguimiento
de las líneas en mapa.
El sensor de Color NXT funciona de la siguiente manera:
Se conecta a un puerto de sensores del NXT mediante un cable NXT normal y hace uso
del protocolo digital de comunicaciones I2C. El Número de Color calculado por el sensor se
refresca aproximadamente 100 veces por segundo.
Este sensor incorpora tres LEDs (RGB: red, gren ,blue) de distinto color que iluminan la
superficie cuyo color desea detectarse. Se mide la intensidad que esta superficie refleja para
cada uno de los colores y , Mediante el valor de la intensidad relativa reflejada de cada uno
de los colores, el sensor de color calcula un Número de Color, que es el valor que se devuelve
al programa NXT.
El sensor de color RGB se puede utilizar en tres Modos:
Modo sensor de color, usando el software estándar, puede detectar seis colores: negro,
blanco, rojo, verde, azul y amarillo
Modo lámpara: es posibe controlar los LED’s del sensor como verde, rojo y amarillo
6. Lego Mindstorm 31
Modo de sensor de luz: En este modo, actúa como el sensor de luz antigua: devuelve
un valor de 0-100 donde 0 es más oscuro, y el 100 es más brillante. En este modo,
también es posible elegir un LED de color deseado (de nuevo, rojo, azul o verde)
6.2. LEJOS
Dado que Lego provee un entorno propietario cerrado para la programación de la uni-
dad de control del Lego es necesario realizar una re configuración de la unidad de control
reemplazando su sistema operativo si se quiere desarrollar aplicativos utilizando otras he-
rramientas o lenguajes como por ejemplo Java.
Para el desarrollo de los drivers se ha escogido utilizar Lejos que es una pequeña má-
quina virtual Java que se instala en la unidad de control Lego y permite el desarrollo y
ejecución de aplicativos escritos en Java dentro de esta unidad de control. Lejos expone una
API que permite el control del hardware provisto por Lego.
6.3. Construcción
Para poder ejecutar los casos de estudios propuestos en esta tesis utilizando los robots
Lego NXT y EV3 fue necesario construir los agentes autónomos físicos. Por motivos de prac-
ticidad y evitando incorporar variables adicionales a los modelos planteados como ser la
resolución de la posición de los robots, he tomado la decisión de utilizar modelos que se ubi-
can en el terreno siguiendo un camino mediante la lectura del terreno utilizando un lector
óptico RGB.
El modelo del agente construido consta de un sistema de tracción basado en 2 servo-
motor, que mediante las ruedas de tracción, permiten el control direccional del agente. En
el frente central se ubica el lector óptico que sensa constantemente el terreno en busca de
variaciones de color identificando si el lector se encuentra sobre el camino, fuera del camino
o en algún punto de interés como ser una intersección. El cuerpo del agente consta de la
unidad de control programable donde reside el driver encargado de ejecutar los algoritmos
de control y comunicación con el controlador sintetizado.
A continuación se aprecia las unidades construidas para el modelo Lego NXT:
6. Lego Mindstorm 32
Fig. 6.7: Robot NXT
Y el modelo construido para el modelo Lego EV3:
Fig. 6.8: Robot EV3 - Frente
6. Lego Mindstorm 33
Fig. 6.9: Robot EV3 - Atras
6.4. Driver
Para que el robot construido para ejecutar las pruebas de concepto pueda interpretar y
ejecutar las instrucciones primitivas que recibe del controlador sintetizado y a su vez pueda
reportar de regreso el estado del mismo es necesario el desarrollo de un driver que es ejecu-
tado por la unidad de control del Lego.
Este driver consiste en un aplicativo que es ejecutado por Lejos y es el encargado de:
Calibración Al iniciar el driver el mismo ejecuta una secuencia de calibración de los
sensores. El objetivo del mismo obtener las lecturas de referencia según el ambiente
donde se realizará la ejecución.
Comunicación La comunicación con el controlador es a través de Bluetooth. El driver
inicia el canal de comunicación con el controlador y es por este que recibe los comandos
a ejecutar y el driver reporta las condiciones de estado del mismo.
Primitivas las primitivas son los comandos que el robot podrá ejecutar y los mismos
son implementados por el driver. Estas primitivas tienen una relación directa con las
acciones controlables del modelo. Ejemplo de las primitivas implementadas:
• Follow
• TurnRight
• TurnLeft
• TurnAround
Informar cuando se haya alcanzado el objetivo deseado. Por ejemplo avanzar por una
línea hastaun cruce determinado.
Informar condiciones de error como ser que por alguna razón el robot se haya perdido
o algún inconveniente relacionado con el hardware como por ejemplo batería baja.
La figura 6.10 describe la arquitectura propuesta para el adaptador enactment y el
driver instalable en la unidad de control del agente:
6. Lego Mindstorm 34
Fig. 6.10: Arquitectura Enactor NXT y Driver
6.5. Implementación driver
La arquitectura del driver se basa en un diseño de 2 capas. La primera de bajo ni-
vel NXTDriverComm encargada de la comunicación, control de los motores de tracción y
lectura a través del lector óptico. La capa superior NXTDriver es responsable de la codifi-
cación y ejecución de los comandos devolviendo al controlador sintetizado, mediante el canal
de comunicación establecido, los mensajes de estado de ejecución. Adicionalmente esta úl-
tima capa es la encargada de ejecutar la rutina de inicialización que incluye la calibración
del sensor de color sobre el terreno. Esta calibración guía al usuario mediante la interfaz
gráfica que la unidad de control Lego provee para que ubique el lector sobre el camino, fue-
ra de camino e intersecciones con el fin de tomar los valores del terreno y poder con estos
últimos nutrir a los algoritmos de control.
El esquema de funcionamiento sigue el comportamiento “maestro-esclavo”. El agente
recibe las instrucciones enviadas del controlador sintetizado, el agente ejecuta la instrucción
y retorna el valor de estado. El siguiente esquema temporal representa un flujo de ejecucion:
6. Lego Mindstorm 35
Fig. 6.11: Esquema secuencia entre el adaptador y el driver
6.5.1. Comunicación
La comunicación entre el agente y el controlador sintetizado se realiza mediante un
canal Bluethooth. Lego NXT y EV3 provee un dispositivo Bluethooth incorporado en su
unidad de control. El canal establecido es del tipo serial y el protocolo de comunicación
definido sigue los siguientes lineamientos:
Paquetes de longitud fija de 2 bytes representados por enteros
Los paquetes que envia el controlador sintetizado respetan la siguiente codificacion
definidos en RobotDriverCommCommands:
• follow
• turnLeft
• turnRight
• turnAround
Los comandos listados son de longitud fija y los mismos no poseen parametros asocia-
dos.
6. Lego Mindstorm 36
Los codigos definidos para los mensajes de respuesta son los siguientes:
• sucess
• fail
• robotLost
• unsupportedCommand
Los mensajes de respuesta son de longitud fija y no poseen parametros adicionales.
6.5.2. Control
Los comandos implementados en esta tesis que equivalen a los mensajes de control pro-
venientes del controlador sintetizado. Los mismos como se ha mencionado anteriormente
son: follow, turnRight, turnLeft, turnArround. Las rutinas se basan en el caso del follow en
trasladar al robot a través del camino desde una intersección de inicio hacia otra intersec-
ción. Para los comandos de turnRight, turnLeft y turnArround los algoritmos de control se
encargaran de rotar al robot hacia la derecha, izquierda y 180 grados respectivamente.
Cabe destacar que esta rotación adicionalmente tiene en cuenta la re ubicación del ro-
bot nuevamente en la posición de intersección. Esto no es un detalle menor dado que debe
tener en cuenta la geometría del robot construido y dado que el sistema de posicionamiento
solo se basa en la lectura del sensor óptico, el mismo no debe perder el control de donde
se encuentra el camino y la intersección. Dado esta dificultan, los algoritmos implementa-
dos constantemente obtienen las lecturas del sensor a medida que se ejecuta la rotación
del robot y dado el movimiento angular, decide cuando el mismo se encuentra nuevamente
alineado sobre el camino. Como último paso se re ubica el robot sobre la intersección infor-
mando el estado de completitud de la instrucción.
Acerca del algoritmo de seguimiento del camino el algoritmo implementado utiliza téc-
nicas de control continuo para controlar el avance del agente en función de las lecturas
que se toman sobre el lector óptico. Dada la naturaleza de éste último las lecturas que se
obtienen incluyen un ruido considerable que debe filtrarse e implementar mecanismos de
tolerancia con el fin de no tomar decisiones equivocadas acerca de la posición del robot.
El algoritmo implementado para el seguimiento de línea se basa fundamentalmente en
el control continuo utilizando las lecturas del lector RGB que censa regularmente la super-
ficie. Los valores obtenidos alimentan a la función de ajuste
6. Lego Mindstorm 37
offset = (linea + suelo)/2;
constante_ajuste = velMax/(suelo-offset);
...
error = color_lectura - offset;
ajuste = constante_ajuste * error;
Motor.A.setSpeed(Math.round(velMax + ajuste));
Motor.C.setSpeed(Math.round(velMax - ajuste));
Fig. 6.12: Algoritmo de control seguimiento camino
El ajuste se aplica a las velocidades de rotación del motor izquierdo y derecho de mane-
ra inversa. Adicionalmente mitigar el control de ruido en la lectura de colores se incorporó
tolerancia al momento de reconocer si el agente se encuentra fuera del camino.
En caso que el robot se encuentra fuera de camino, se implementó un algoritmo de re-
cuperación que intenta realizar determinados movimientos en una cierta heurística con el
fin de poder reestablecer al lector del agente sobre el camino. En caso que esta heurística
falle el agente reporta un mensaje de estado robotLost que es transmitido al controlador
sintetizado.
Se ha presentado dificultades adicionales sobre el entorno donde el agente desempe-
ñaba las instrucciones siendo las fuentes de luces ambientales el principal responsable en
introducir ruido en las lecturas obtenidas llevando al agente a perder la posición sobre el
terreno reportando un estado de falla (robotLost). En la sección Robustez 6.7 se detalla las
mediciones con resultados estadísticos acerca de las puestas en ejecución del agente en el
terreno utilizando distintos ambientes. De las lecturas obtenidas se han podido observar la
injerencia de la fuente de luz en el ambiente como responsable de la eficacia del agente en
poder reconocer correctamente la ubicación sobre el terreno.
6.6. Entorno para pruebas
Los casos de estudios desarrollados en esta tesis han sido construidos en base a un en-
torno descripto por una superficie donde una serie de caminos dibujados por líneas negras
por donde el agente transitará. Adicionalmente se encuentran una serie de puntos de pa-
rada donde el agente realizará las paradas indicadas con un color que se diferenciará del
fondo del mapa y de los caminos. La traza propuesta describe una serie un cuadrado interior
con puntos de paradas en sus esquinas y con caminos circulares de inicio y fin desde cada
uno de los puntos de parada como indica la siguiente figura 6.13:
6. Lego Mindstorm 38
Fig. 6.13: Mapa Infinito
6.7. Robustez – Estadísticas
La robustez del diseño planteado por el hardware subyacente puede ser medida en uno
de sus aspectos por la ejecución satisfactoria por parte del robot de las instrucciones primi-
tivas. La ejecución y performance de las operaciones dependen de la correcta lectura de los
sensores, en especial para los casos de estudios planteados en este trabajo depende directa-
mente del sensor óptico utilizado para el reconocimiento del camino.
Se realizaron una serie de pruebas para determinar cuan eficiente es el lector óptico
y cuan robusto es el robot a la hora de reconocer los caminos e intersecciones del mapa.
Debido a que la luminosidad del ambiente tiene un impacto directo en el rendimiento del
sensor óptico, se han tomado las muestras para distintos escenarios lumínicos:
luz día
luz tubo fluorescente
incandescente
oscuridad
6.7.1. Medición
La medida utilizada para evaluar la performance del lector ha sido cantidad de opera-
ciones primitivas realizadas (follow, turnRight, turnLeft, turnAround).
6.7.2. Escenario de pruebas
El escenario escogido para el ensayo es una configuración de un “mapa infinito”. El mis-
mo tiene como particularidad que