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
  • Promote your Publication

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
  • Proposals
  • Guest Editors

Future of Information and Communication Conference (FICC)

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

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
  • Home
  • Call for Papers
  • Indexing
  • Submit your Paper
  • Guidelines
  • Fees
  • Current Issue
  • Archives
  • Editors
  • Reviewers
  • Subscribe

DOI: 10.14569/IJACSA.2018.091071

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

PDF

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}
}



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.

IJACSA

Upcoming Conferences

Future of Information and Communication Conference (FICC) 2024

4-5 April 2024

  • Berlin, Germany

Computing Conference 2024

11-12 July 2024

  • London, United Kingdom

IntelliSys 2023

7-8 September 2023

  • Amsterdam, The Netherlands

Future Technologies Conference (FTC) 2023

2-3 November 2023

  • San Francisco, United States
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. All rights reserved. Registered in England and Wales. Company Number 8933205. thesai.org