La construcción de software complejo puede verse asistida por los llamados métodos formales que permiten detectar errores de diseño e implementación, especialmente con respecto a las propiedades críticas del sistema. Los métodos formales son técnicas con una base matemática muy fuerte que les hace muy apropiados para el análisis y verificación del software. En este proyecto, hemos seleccionado un sistema complejo, como es la construcción de un sistema compuesto de varios ascensores que funcionan de manera coordinada. Este problema muestra muchos de los problemas típicos del desarrollo de software crítico. Por un lado, como cada ascensor funciona como un proceso autónomo que tiene que sincronizarse con el resto, la implementación del sistema puede contener los típicos errores de seguridad o viveza propios de los sistemas concurrentes. Por otro lado, la estructura del sistema de ascensores contiene varios componentes que se relacionan entre sí de múltiples formas. Finalmente, en el sistema de ascensores también hay propiedades de tiempo real que deberían satisfacerse para que su comportamiento sea aceptable. Cada tipo de propiedad requiere utilizar una técnica formal diferente. La mejor técnica formal para detectar errores propios de la interacción incorrecta entre procesos es el “Model Checking”[1,2,3]. En el model checking, los actores principales son los estados del sistema, y las transiciones que hacen que el sistema evolucione. Sin embargo, para analizar propiedades estructurales de los sistemas es mucho más fácil y eficiente usar lenguajes en los que la noción de clase y relación/asociación sea más explícita. En este proyecto, se ha utilizado el model checker SPIN, las herramientas Alloy, USE (para UML/OCL) y Uppaal para la descripción y análisis de las distintas propiedades deseables del sistema. Como resultado, se ha construido un sistema de ascensores que es correcto con respecto a las propiedades críticas del sistema.
Buscar en Dimension
