An Spin / Promela application for model checking UML sequence diagrams

Vidal-Silva C.L.; Villarroel R.; Rubio J.; Johnson F.; Madariaga E.; Campos C.; Carter L.

dc.contributor.author	Vidal-Silva C.L.
dc.contributor.author	Villarroel R.
dc.contributor.author	Rubio J.
dc.contributor.author	Johnson F.
dc.contributor.author	Madariaga E.
dc.contributor.author	Campos C.
dc.contributor.author	Carter L.
dc.date.accessioned	2020-09-02T22:30:04Z
dc.date.available	2020-09-02T22:30:04Z
dc.date.issued	2018
dc.identifier	10.14569/IJACSA.2018.091071
dc.identifier.citation	9, 10, 586-599
dc.identifier.issn	2158107X
dc.identifier.uri	https://hdl.handle.net/20.500.12728/6563
dc.description	UML 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. © 2015 The Science and Information (SAI) Organization Limited.
dc.language.iso	en
dc.publisher	Science and Information Organization
dc.subject	Combined Fragment
dc.subject	Fault Tolerance
dc.subject	LTL formulas
dc.subject	Spin / Promela
dc.subject	UML Sequence Diagrams
dc.title	An Spin / Promela application for model checking UML sequence diagrams
dc.type	Article