Una técnica para una especificación inicial en RSL

Abstract

Los métodos formales ayudan a incrementar la confiabilidad del software. Estos métodos permiten “razonar” acerca de propiedades del software o de sistemas que involucran software. Además, ofrecen la seguridad de que los requisitos son verificados en cada paso del desarrollo, encontrando inconsistencias e incompletitud. Las especificaciones formales se pueden usar durante todo el ciclo de vida del software y se pueden manipular con herramientas automáticas con una amplia variedad de propósitos tales como model checking, verificación deductiva, animación, generación de casos de prueba, reuso formal de componentes, y refinamiento de especificación a implementación. El Método RAISE (Rigourous Approach to Industrial Software Engineering) [3], por ejemplo, provee facilidades para el uso industrial de métodos formales en el desarrollo de sistemas de software. Este método provee de un gran número de técnicas y estrategias para hacer desarrollos formales y pruebas, además de un lenguaje formal de especificación, RAISE Specification Language (RSL) [2], y un conjunto de herramientas. Sin embargo, estos métodos son, en general, sólo accesibles a especialistas debido a que sus formalismos matemáticos son más difíciles de entender y comunicar.