TY - JOUR
T1 - Una propuesta de algoritmo spin / promela para el análisis y diagnóstico de errores en diagramas de secuencia UML
AU - Vidal-Silva, Cristian L.
AU - Villarroel, Rodolfo H.
AU - López-Cortés, Xaviera A.
AU - Rubio, José M.
N1 - Funding Information:
Aun cuando la figura 1 representa un ejemplo básico de escenario para la secuencia de interacción entre objetos, tal como presenta la figura 2, dichos escenarios pueden también corresponder al detalle de interacción de los objetos involucrados a un caso de uso. Los diagramas de secuencia UML, diagramas de estado y diagramas de colaboración permiten modelar el comportamiento de los casos de uso de sistemas de software (Miles y Hamilton, 2006). Sin embargo, la diferencia principal y la ventaja potencial de los diagramas de secuencia UML con respecto a los otros diagramas UML para modelar el comportamiento son que los primeros establecen escenarios que usualmente involucran a más de un objeto del sistema. Si bien, posiblemente haya un gran número, posiblemente infinito, de escenarios en un sistema de software, es relevante modelar situaciones críticas para describir esos escenarios con sus instancias participantes y la comunicación entre ellos, y así, después de revisar esas interacciones, poder establecer posibles estados de los objetos participantes, y entonces deducir condiciones y acciones que producen cambio de estado en dichos objetos. Por lo tanto, los diagramas de secuencia UML permiten la generación de diagramas de estados UML (Pender, 2003). Claramente, esto último representa una característica positiva del uso de diagramas de secuencia UML. Además, con la mencionada propiedad de modelar comportamiento algorítmico mediante fragmentos combinados, y la capacidad de traducirlos a código Spin / Promela para detectar y corregir fallas, definitivamente los diagramas de secuencia UML son una gran herramienta para producir modelos de software de calidad.
Publisher Copyright:
© 2019 Centro de Informacion Tecnologica. All Rights Reserved.
PY - 2019/2
Y1 - 2019/2
N2 - This paper describes the main characteristics of UML sequence diagrams, the notion of failure or error and fault tolerance, and some common fault types and their correction actions in a UML sequence diagram. Thus, the main objective of this work is to propose an algorithm for the transformation of UML sequence diagrams in Spin / Promela code, a formal verification and errors detection in the model checking for a fault tolerance system, and thus to provide explanations of the necessary steps to adjust and corrections the affected diagrams. The algorithm for transforming UML sequence diagrams into Spin / Promela code is useful for the detection of faults in sequence of messages. The proposed solution is applied on a simple and general UML sequence diagram to analyze its Promela code, guarantying in this way the model checking effectiveness on UML sequence diagrams. This work also presents ideas to extend the proposal for the analysis of UML sequences diagrams which include combined fragments of iterations.
AB - This paper describes the main characteristics of UML sequence diagrams, the notion of failure or error and fault tolerance, and some common fault types and their correction actions in a UML sequence diagram. Thus, the main objective of this work is to propose an algorithm for the transformation of UML sequence diagrams in Spin / Promela code, a formal verification and errors detection in the model checking for a fault tolerance system, and thus to provide explanations of the necessary steps to adjust and corrections the affected diagrams. The algorithm for transforming UML sequence diagrams into Spin / Promela code is useful for the detection of faults in sequence of messages. The proposed solution is applied on a simple and general UML sequence diagram to analyze its Promela code, guarantying in this way the model checking effectiveness on UML sequence diagrams. This work also presents ideas to extend the proposal for the analysis of UML sequences diagrams which include combined fragments of iterations.
KW - Fault tolerance
KW - Models analysis
KW - Sequence diagrams
KW - Spin / Promela
KW - UML
UR - http://www.scopus.com/inward/record.url?scp=85057269618&partnerID=8YFLogxK
U2 - 10.4067/S0718-07642019000100263
DO - 10.4067/S0718-07642019000100263
M3 - Article
AN - SCOPUS:85057269618
VL - 30
SP - 263
EP - 272
JO - Informacion Tecnologica
JF - Informacion Tecnologica
SN - 0716-8756
IS - 1
ER -