
ISBN: 978-84-1142-201-7
© Juan Antonio Carrasco Domínguez
Importancia de las herramientas de model checking para la resolución de conflictos en aspectos de gestión
Introducción
Este primer capítulo tratará de mostrar los problemas que han surgido en cuanto a aspectos de gestión no funcionales en la computación, así como diversas formas de solucionarlo. Además se profundizará en una de estas soluciones, que hará patente la necesidad de un traductor de Appel.
Problemas surgidos en aspectos no funcionales en la computación
Durante los últimos años, la computación ha experimentado un desarrollo orientado hacia el trabajo en red o en la nube, lo cual nos lleva a sistemas que deben ser mucho más adaptables. Esto tiene una gran importancia en cuanto a los aspectos no funcionales de la computación como por ejemplo la seguridad, el rendimiento o el consumo de energía.
Para hacer frente a este problema se plantea crear un esqueleto formado por todos estos aspectos no funcionales, los cuales estarán bajo la monitorización de un gestor, que también tendrá capacidad para realizar cambios en este esqueleto.
El problema surge cuando el gestor de uno de estos aspectos, entra en conflicto con otro de los gestores, pongamos un ejemplo simple: tengamos un computador con más de un núcleo, que está monitorizado por dos gestores, uno monitoriza la energía consumida, y otro la carga de cómputo de cada uno de los núcleos de su procesador. El primer gestor visualiza que se está consumiendo mucha energía, por lo tanto va a desactivar uno de estos núcleos, pero simultáneamente el segundo gestor detecta un descenso en el rendimiento de cómputo, por lo tanto va a activar otro núcleo del procesador. Lo cual produce un conflicto.
Lo que se pretende es evitar estos conflictos, esta tarea puede realizarse o bien manualmente, o bien gracias a un model checker, el cual será capaz de detectar todos los conflictos y el origen que los provocó.
Gestión basada en reglas
El funcionamiento del esqueleto es básicamente el siguiente, el gestor monitoriza cierto aspecto, comprueba si debe ser modificado y finalmente ejecuta la modificación para volver a comenzar. Es el clásico bucle MAPE, el cual puede ser implementado como un conjunto de reglas formadas por precondiciones y acciones.
Resulta evidente que para cada aspecto no funcional, tendremos un gestor experto en ese aspecto, por tanto el problema será al coordinar a estos gestores. Para ello tenemos que evitar que en un mismo ciclo del bucle MAPE dos gestores traten de ejecutar modificaciones contrapuestas, como por ejemplo añadir procesador, eliminar procesador. Para realizar esta tarea nos facilitará mucho el trabajo el tener un gráfico de la aplicación, que nos muestre la evolución de nuestro sistema, y donde podamos detectar los conflictos; donde cada nodo del gráfico representará una acción y cada arco representará la comunicación o sincronización.
Índice
1 Importancia de las herramientas de model checking para la resolución de conflictos en aspectos de gestión
1.1 Introducción
1.2 Problemas surgidos en aspectos no funcionales en la computación
1.3 Gestión basada en reglas
1.4 Opciones de gestión de no funcionales
1.5 Por qué usar un model checker
1.6 Justificación de la herramienta de traducción automática y aspectos básicos de la misma
2 Traducción de Appel a UML
2.1 Introducción
2.2 El lenguaje Appel
2.3 Mapeo de Appel a UML
2.4 Mapeo de una regla simple de Appel
2.5 Mapeo de una regla compuesta de Appel
3 Declaración de una sintaxis textual para UML
3.1 Introducción
3.2 Declaración de estados
3.3 Declaración de transiciones
4 Decisiones de diseño
4.1 Programación funcional
4.2 El lenguaje OCAML
4.3 Arquitectura básica del traductor
4.3.1 Translator.
4.4 Unparser
4.4.1 El model checker UMC
4.5 Definición de la sintaxis Appel en Ocaml
4.6 Definición de la sintaxis UML en OCaml
4.7 Herramientas adicionales
4.7.1 Size
4.7.2 DomainCreator
5 Manual de usuario
5.1 Introducción
5.2 Requisitos básicos
5.3 Como usar el Traductor de Appel
5.3.1 Traducción a UML
5.3.2 Traducción a UMC
5.3.3 Valor de la Size
5.3.4 Generador del archivo de dominio
5.4 Carga en modo recuperación
5.5 El archivo de configuración
5.6 Archivo de configuración de recuperación
5.7 Archivo de dominio
5.8 Detalles de entrada y salida
5.8.1 Gramática de entrada: Appel
5.8.2 Gramática de salida: UML
5.8.3 Gramática de salida: UMC
5.9 Archivo de condiciones 40
6 Manual de mantenimiento
6.1 Propósito de este manual
6.2 ¿Qué es el traductor de Appel?
6.3 ¿Cómo está hecho el traductor?
6.4 Estructura del compilador.
6.4.1 Archivos externos
6.4.2 Kernel
6.5 Pruebas
7 Apéndice: Size
7.1 Size
7.2 Reglas simples
7.2.1 AndThen
7.2.2 OrElse
7.2.3 Or
7.2.4 And
7.2.5 Ejemplo de una acción compuesta de manera heterogénea
7.3 Reglas compuestas: reglas en paralelo
Lista de referencias