A Spin / Promela Application for Model checking UML Sequence Diagrams

Simple item page
dc.contributor.authorVidal-Silva, Cristian
dc.contributor.authorVillarroel, Rodolfo
dc.contributor.authorRubio, José Miguel
dc.contributor.authorJohnson, Franklin
dc.contributor.authorMadariaga, Erika
dc.contributor.authorCampos, Camilo
dc.contributor.authorCarter, Luis
dc.date.accessioned2019-07-15T08:10:52Z
dc.date.available2019-07-15T08:10:52Z
dc.date.issued2018
dc.description.abstractUML sequence diagrams usually represent the behavior of systems execution. Automated verification of UML sequence diagrams’ correctness is necessary because they can model critical algorithmic behaviors of information systems. UML sequence diagrams applications are often on the requirement and design phases of the software development process, and their correctness guarantees the accurate and transparent implementation of software products. The primary goal of this article is to review and improve the translation of basic and complex UML sequence diagrams into Spin / Promela code taking into account behavioral properties and elements of combined fragments of UML sequence diagrams for synchronous and asynchronous messages. This article also redefines a previous proposal for a transition system for UML sequence diagrams by specifying Linear Temporal Logic (LTL) formulas to verify the model correctness. We present an application example of our modeling proposal on a modified version of a traditional case study by using UML sequence diagrams to translate it into Promela code to verify their properties and correctness.es_ES
dc.identifier.issn2156-5570
dc.identifier.other10.14569/IJACSA.2018.091071
dc.identifier.urihttps://hdl.handle.net/20.500.12536/105
dc.language.isoenes_ES
dc.sourceInternational Journal of Advanced Computer Science and Applications (IJACSA)es_ES
dc.subjectSpin / Promelaes_ES
dc.subjectUML Sequence Diagramses_ES
dc.subjectFault tolerancees_ES
dc.subjectLTL formulases_ES
dc.subjectCombined fragmentes_ES
dc.titleA Spin / Promela Application for Model checking UML Sequence Diagramses_ES
dc.typeArtículo de revistaes_ES
uvm.carreraIngeniería Civil Informáticaes_ES
uvm.escuelaEscuela de Ingenieríaes_ES
uvm.indexScopuses_ES
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
An Spin Promela Application for Model checking UML Sequence Diagrams.pdf
Size:
809.67 KB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
Artículos científicos