The Science and Information (SAI) Organization
  • Home
  • About Us
  • Journals
  • Conferences
  • Contact Us

Publication Links

  • IJACSA
  • Author Guidelines
  • Publication Policies
  • Metadata Harvesting (OAI2)
  • Digital Archiving Policy

IJACSA

  • About the Journal
  • Call for Papers
  • Author Guidelines
  • Fees/ APC
  • Submit your Paper
  • Current Issue
  • Archives
  • Indexing
  • Editors
  • Reviewers
  • Apply as a Reviewer

IJARAI

  • About the Journal
  • Archives
  • Indexing & Archiving

Special Issues

  • Home
  • Archives
  • Call for Papers
  • Proposals
  • Guest Editors

Computing Conference

  • Home
  • Call for Papers
  • Submit your Paper/Poster
  • Register
  • Venue
  • Contact

Intelligent Systems Conference (IntelliSys)

  • Home
  • Call for Papers
  • Submit your Paper/Poster
  • Register
  • Venue
  • Contact

Future Technologies Conference (FTC)

  • Home
  • Call for Papers
  • Submit your Paper/Poster
  • Register
  • Venue
  • Contact

Future of Information and Communication Conference (FICC)

  • Home
  • Call for Papers
  • Submit your Paper/Poster
  • Register
  • Venue
  • Contact
  • Home
  • Call for Papers
  • Guidelines
  • Fees
  • Submit your Paper
  • Current Issue
  • Archives
  • Indexing
  • Editors
  • Reviewers
  • Subscribe

Article Details

Copyright Statement: This is an open access article licensed under a Creative Commons Attribution 4.0 International License, which permits unrestricted use, distribution, and reproduction in any medium, even commercially as long as the original work is properly cited.

An Spin / Promela Application for Model checking UML Sequence Diagrams

Author 1: Cristian L. Vidal-Silva
Author 2: Rodolfo Villarroel
Author 3: Jos´e Rubio
Author 4: Franklin Johnson
Author 5: Erika Madariaga
Author 6: Camilo Campos
Author 7: Luis Carter

Download PDF

Digital Object Identifier (DOI) : 10.14569/IJACSA.2018.091071

Article Published in International Journal of Advanced Computer Science and Applications(IJACSA), Volume 9 Issue 10, 2018.

  • Abstract and Keywords
  • How to Cite this Article
  • {} BibTeX Source

Abstract: 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 implemen-tation 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.

Keywords: Spin / Promela; UML Sequence Diagrams; Fault Tolerance; LTL formulas; Combined Fragment

Cristian L. Vidal-Silva, Rodolfo Villarroel, Jos´e Rubio, Franklin Johnson, Erika Madariaga, Camilo Campos and Luis Carter, “An Spin / Promela Application for Model checking UML Sequence Diagrams” International Journal of Advanced Computer Science and Applications(IJACSA), 9(10), 2018. http://dx.doi.org/10.14569/IJACSA.2018.091071

@article{Vidal-Silva2018,
title = {An Spin / Promela Application for Model checking UML Sequence Diagrams},
journal = {International Journal of Advanced Computer Science and Applications},
doi = {10.14569/IJACSA.2018.091071},
url = {http://dx.doi.org/10.14569/IJACSA.2018.091071},
year = {2018},
publisher = {The Science and Information Organization},
volume = {9},
number = {10},
author = {Cristian L. Vidal-Silva and Rodolfo Villarroel and Jos´e Rubio and Franklin Johnson and Erika Madariaga and Camilo Campos and Luis Carter}
}


IJACSA

Upcoming Conferences

Future of Information and Communication Conference (FICC) 2023

2-3 March 2023

  • Hybrid | San Francisco

Computing Conference 2023

13-14 July 2023

  • Hybrid | London, UK

IntelliSys 2022

1-2 September 2022

  • Hybrid / Amsterdam

Future Technologies Conference (FTC) 2022

20-21 October 2022

  • Hybrid / Vancouver
The Science and Information (SAI) Organization
BACK TO TOP

Computer Science Journal

  • About the Journal
  • Call for Papers
  • Submit Paper
  • Indexing

Our Conferences

  • Computing Conference
  • Intelligent Systems Conference
  • Future Technologies Conference
  • Communication Conference

Help & Support

  • Contact Us
  • About Us
  • Terms and Conditions
  • Privacy Policy

© The Science and Information (SAI) Organization Limited. Registered in England and Wales. Company Number 8933205. All rights reserved. thesai.org