Integración efectiva de paradigmas de especificación de software

Abstract

La especificación como una forma de descripción del comportamiento del software se ha vuelto un tanto subjetiva; esta subjetividad ha conllevado la creación de diferentes paradigmas de especificación, siendo los dos paradigmas más importantes: el paradigma que utiliza modelos diagramáticos y el paradigma que utiliza la descripción formal. Ambos paradigmas han evolucionado de una manera separada; por un lado, se tiene la facilidad de elaborar diagramas y comunicar visualmente, por otro lado la posibilidad de describir formalmente el software mediante notaciones matemáticas precisas. Debido a esta separación es necesario establecer un marco de referencia que promueva la integración entre estos paradigmas de manera que se pueda utilizar las ventajas de ambos. Tal marco de referencia requiere conciliar la especificación diagramática y la formal. Para establecer este marco conviene delimitarlo a un área de trabajo que sea común a cualquier esfuerzo de desarrollo de software; la parte más idónea es la base de la arquitectura del software que se refiere al modelado de datos. El modelado de datos se hace comúnmente por medio del modelo entidad-relación y permite establecer asociaciones entre entidades que tienen atributos. Es importante destacar que dentro del modelo entidad-relación existen diferentes notaciones, siendo las más utilizadas las que manejan cardinalidades máximas y mínimas. La parte estática del modelado de datos corresponde a la definición de datos en lenguaje Z; además, se puede especificar la parte dinámica por medio de esquemas de operaciones en Z y que el usuario pueda extender la especificación en lo que se refiere a invariantes, precondiciones y postcondiciones. Debido a lo anterior, este trabajo propone un marco de referencia común para el modelo entidad-relación y el lenguaje Z que permite integrar de manera efectiva ambos paradigmas de especificación. Para comprobar dicho marco de referencia se desarrolló una herramienta de software basada en Web que facilita hacer la transformación automática del modelo entidad-relación a su equivalente en lenguaje Z en dos formatos: en PDF para una vista inmediata y en TEX para permitir aumentar la especificación y utilizar algún verificador de tipos como FUZZ, así como su edición con formatos precisos para la publicación.

The specification as a way of describing the behavior of software has become somewhat subjective; this subjectivity has led to the creation of different specification paradigms, the two major ones being diagrammatic models and formal description. Both paradigms have evolved separately; on the one hand, it is easy to draw diagrams and to communicate visually. On the other hand, there is the opportunity to formally describe the software using precise mathematical notations. Because of this separation, it is desirable to establish a framework that promotes the integration of these paradigms in order to use the advantages of both. Such a framework requires reconciling diagrammatic and formal specifications. To establish this connection, it is convenient to delimit it to an area of software development and the most suitable one is data modeling which is one of the foundations of software architecture. Data modeling here is done using the entity-relationship model, which comprises associations between entities that have attributes. There are several entity-relationship modeling notations, the most popular being those that let specify maximum and minimum cardinalities in associations. The static part of data modeling corresponds to the definition of data in Z (with schema types). Furthermore, the functional requirements can be specified through operations in Z. The user can then extend the specification in regard to invariants (of data types), preconditions and post conditions (of operations). This document proposes a common framework for entity-relationship visual modeling and formal description in the Z language that allows effectively integrating both paradigms of specification. To validate this framework, we developed a Web-based software tool that facilitates to automatically translate entity-relationship models into their Z-language equivalents, using two formats: PDF for immediate reading and TEX, in order to enable augmenting the specification and using tools such as the FUZZ type-checker and tools for precise editing of documents in formats suitable for publication.