Metamodel-Based Model Conformance and Multiview Consistency Checking

Paige et al. [1] presentan una investigación donde comparan dos lenguajes (UML y BON [2]) para el modelado de sistemas, así como sus respectivas consistencias entre múltiples vistas del sistema, es decir, si un diagrama (estructural por ejemplo, el caso de diagramas de clases) es consistente y refleja el mismo sistema modelado a partir de otro diagrama (de comportamiento, por ejemplo, diagramas de secuencia).

Su investigación incluye una breve y no formal revisión de los conceptos sobre el modelado de sistemas en BON y su relación con el lenguaje de programación Eiffel [3] para el manejo de contratos, y por otra parte una revisión de UML 2.0 y OCL 2.0. Además, mencionan algunas ventajas y desventajas de ambos, por mencionar unas, para el caso de BON y Eiffel son lenguajes no tan difundidos como UML y OCL, no obstante, proveen una semántica más formal (aunque incompleta) que éstos últimos.

Indican también, siete criterios a considerar para las técnicas de meta-modelado y el multiview consistency checking (MVCC), a saber:

1) comprensibilidad (understandability) que implica que las descripciones usadas son entendibles para un ingeniero de software con una experiencia razonable en lenguajes de modelados pero no necesariamente experiencia en métodos formales;
2) correctitud (correctness), esto es, que las descripciones del meta-modelo sean verificadas contra sus especificaciones;
3) completitud (completeness) es decir, todas las características del lenguaje de modelado (incluyendo restricciones de consistencias entre múltiples vistas) son soportadas por la técnica de meta-modelado;
4) mantenibilidad (maintainability) esto implica que las descripciones soporten extensión, refactorización y en caso de requerirse, modificaciones completas;
5) herramientas de soporte (tool construction) lo que representa que existan y/o puedan desarrollarse herramientas que faciliten la producción de las descripciones;
6) verificación y validación basadas en herramientas (tool-based V&V) es decir, que existan y/o puedan desarrollarse herramientas que puedan asistir en la verificación y validación de las descripción y
7) automatización en MVCC (automation in MVCC), que la consistencia entre múltiples vistas pueda ser verificada de manera automática.

Los autores concluyen en lo que, con la lectura minuciosa de la investigación se puede entrever: no existe una técnica definitiva para el meta-modelado y por ende, para el MVCC, que sea suficiente. Más bien, lo que a algunos lenguajes de modelado les falta, otros lo cubren y viceversa. Sin embargo, de acuerdo con los autores, pareciera ser que UML parece ser más factible de ser más estudiado y explotado dado su grado de madurez y pese a su informal concepción ya que se han hecho esfuerzos en este sentido, es decir, formalizar la especificación de UML.

Indican además, que no siempre es preferible un lenguaje de meta-modelado más expresivo que uno menos expresivo. PVS [4] es más expresivo que BON y Eiffel, y puede capturar todas las reglas de bien-formidad (well-formedness), sin embargo, lo que ofrece en completitud, lo pierde en términos de automatización y facilidad de uso. Eiffel, como lenguaje de meta-modelado, es incompleto pero aún puede ser usado para capturar y verificar casi todas las reglas de well-formedness de manera automática.

Para concluir, y como los propios autores lo mencionan, la investigación provee elemento cualitativos y comparaciones no tan formales y/o cuantitativas, por lo que recomiendan un conjunto de comparaciones más cuantitativas.

Referencias

[1] R.F. Paige, P.J. Brooke y J.S. Ostroff. Metamodel-Based Model Conformance and Multiview Consistency Checking. ACMTransactions on Software Engineering and Methodology,Vol. 16, No. 3, Article 11, Publication date: July 2007.

[2] K. Walden y J. Nerson. 1995. Seamless Object Oriented Software Architecture. PrenticeHall.

[3] Eiffel Software. Eiffel Software
http://www.eiffel.com/

[4] S. Owre, N. Shankar, J. Rushby y D. Stringer-Calvert. 1999. PVS Language Reference.
http://pvs.csl.sri.com

Formalizing and Validating UML Architecture Description of Web Systems

Claramente es una extensión del trabajo anteriormente mostrado. Bajo el concepto de SO-SAM, esta vez Fu et al. [1] muestran cómo a partir de diagramas de estados y diagramas de secuencias modelados en UML, generan RdP y fórmulas de lógica temporal respectivamente.

Para cada uno de los diagramas involucrados, es decir, diagramas de estado y diagramas de secuencia, proponen reglas para sus respectivas transformaciones a RdP y fórmulas de lógica temporal. No obstante, señalan la inherente imposibilidad de probar la correctitud de las transformaciones, sin embargo, validan cuidadosamente la completitud y consistencia de sus reglas de transformación.

Para demostrar su propuesta proponen un caso de estudio que consiste en el procesamiento de imágenes usadas en aplicaciones Web distribuidas. La validación de su técnica se encuentra implícitamente en los métodos formales utilizados (RdP y lógica temporal) y desarrollan su propuesta a través del lenguaje Maude [2].

De acuerdo con los autores, los resultados presentados, muestran que es posible verificar propiedades estructurales y de comportamiento de los sistemas. Finalmente concluyen que su técnica combina los beneficios de UML (fácil de entender y numerosas herramientas de soporte) y la fácil manera de análisis de SO-SAM. Indican además, que el costo de su propuesta se centra en básicamente tres partes: la construcción de especificaciones algebraicas, la generación de redes de alto nivel a partir de los diagramas de estado y la creación de fórmulas basadas en lógica temporal a partir de los diagramas de secuencia.

Referencias

[1] Y. Fu, Z. Dong y X. He. Formalizing and Validating UML Architecture Description of Web Systems. ICWE’06 Workshops, July 1014, 2006, Palo Alto, California, USA. ACM 1595934359/06/07.

[2] Department of Computer Science, University of Illinois at Urbana-Champaign. The Maude System.
http://maude.cs.uiuc.edu/

An Approach to Web Services Oriented Modeling and Validation

Los autores de este paper proponen una técnica de modelación y validación formal basada en redes de Petri (RdP) y lógica temporal para aplicaciones Web. Para llevar esto acabo, Fu et al. [1] extienden el concepto de Modelo de Arquitectura de Software (SAM [2] por sus siglas en inglés, Software Architecture Model) a lo que denominan SO-SAM (Service Oriented-SAM).

La revisión de trabajos relacionados, demuestran, informalmente, que los lenguajes y/o tecnologías adyacentes a XML (SOAP [3], BPEL4WS [4], WSDL [5], WSFL [6], DAML-S [7], WSCL [8], WSCI [9]) no cubren aspectos estructurales y/o de comportamiento y a la vez, propiedades de los sistemas, por lo que proponen SO-SAM con lo pretenden resolver esto a través de las RdP para modelar la estructura y comportamiento dinámico de un sistema y por otro lado lógica temporal para modelar sus propiedades y características del mismo sistema.

Después de la revisión de trabajos relacionados, definen, formalmente cada elemento de SO-SAM, empezando precisamente con la definición formal de dicho concepto. Definen el concepto de puerto en SOSAM, componente, red de servicios y servicio Web.

Presentan un caso de estudio que consiste en un proceso de comercio electrónico y posteriormente plantean la estructura de un parser para SAM, cuyo archivo de entrada es como se espera, un archivo XML. En el archivo XML se define el comportamiento del sistema a través de RdP definidas en Petri Net Markup Language (PNML) [10] y las propiedades del sistema en lógica temporal. La estructura de verificación en tiempo de ejecución usando SAM es mostrada en la figura 1.

Los resultados presentados en este trabajo, demuestran que la generación de código a partir del modelo SAM hacia el parser toma alrededor de 1.5 segundos en una Pentium IV a 2.4Ghz y 512MB RAM. Concluyen con la aseveración de que el comportamiento de sistemas puede ser modelado con RdP y simulado para permitir análisis avanzados, correcciones y más refinamientos, y que con las propiedades especificadas en fórmulas de lógica temporal, el modelo puede ser validado contra estas propiedades. Como resultado, mencionan que su técnica de modelado y validación ayuda a extender la confiabilidad de aplicaciones orientadas a servicios.

Para concluir, los autores se encuentran desarrollando una herramienta que soporte la transferencia automática del modelo SO-SAM a su respectiva especificación en XML. Como trabajo futuro incluyen una ingeniería de automatización que traduzca servicios Web escritos en WSDL a SO-SAM, y construir modelos SO-SAM para aplicaciones en tiempo real.

Referencias

[1] Y. Fu, Z. Dong y X. He. An Approach to Web Services Oriented Modeling and Validation. IW-SOSE’06, May 27-28, 2006, Shanghai, China.

[2] X. He y Y. Deng. A Framework for Specifying and Verifying Software Architecture Specifications in SAM. Volume 45 of The Computer Journal, pages 111–128, 2002.

[3] Simple Object Access Protocol (SOAP), W3C Note 08.
http://www.w3.org/TR/SOAP/

[4] Business Process Execution Language for Web Services (BPEL4WS).
http://www.ibm.com/developerworks/library/ws-bpel

[5] Web Services Description Language (WSDL) 1.1.
http://www.w3.org/TR/wsdl

[6] IBM Corporation. Web Services Flow Language (WSFL) 1.1.
http://www-3.ibm.com/software/solutions/webservices/pdf/WSFL.pdf

[7] A. Ankolekar. DAML-S: Web Service Description for the Semantic Web, 2002.

[8] Web Service Conversation Language (WSCL) 1.0.
http://www.w3.org/TR/2002/NOTE-wscl10-20020314/

[9] Web Service Choreography Interface (WSCI) 1.0.
http://www.w3.org/TR/2002/NOTE-wsci-20020808/

[10] J. Billington, S. Christensen, et al. The Petri Net Markup Language: Concepts, Technology, and Tools. In Proceedings of the 24th International Conference on Applications and Theory of Petri Nets (ICATPN 2003). Volume 2679 of Lecture Notes in Computer Science, pages 483–505. Springer-Verlag, June 2003.