Una propuesta de algoritmo spin / promela para el análisis y diagnóstico de errores en diagramas de secuencia UML

Translated title of the contribution: An spin / PrOMELA algorithm proposal for the analysis and errors diagnosis in UML sequence diagrams

Cristian L. Vidal-Silva, RODOLFO HUMBERTO VILLARROEL ACEVEDO, Xaviera A. López-Cortés, José M. Rubio

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

Abstract

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.

Translated title of the contributionAn spin / PrOMELA algorithm proposal for the analysis and errors diagnosis in UML sequence diagrams
Original languageSpanish
Pages (from-to)263-272
Number of pages10
JournalInformacion Tecnologica
Volume30
Issue number1
DOIs
StatePublished - 1 Feb 2019

Fingerprint Dive into the research topics of 'An spin / PrOMELA algorithm proposal for the analysis and errors diagnosis in UML sequence diagrams'. Together they form a unique fingerprint.

Cite this