An Spin / Promela Application for Model checking UML Sequence Diagrams
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2018, Vol 9, Issue 10
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.
Authors and Affiliations
Cristian L. Vidal-Silva, Rodolfo Villarroel, Jos´e Rubio, Franklin Johnson, Erika Madariaga, Camilo Campos, Luis Carter
Keywords
Related Articles
- EP ID EP408917
- DOI 10.14569/IJACSA.2018.091071
- Views 90
- Downloads 0
QVT transformation by modelling - From UML Model to MD Model
To provide a complete analysis of the organization, its business and its needs, it is necessary for leaders to have data that help decision making. Data warehouses are designed to meet such needs; they are an analysis an...
Non-Linear Distance Transformation Algorithm and its Application in Medical Image Processing in Healthcare
Medical image processing is one of the most demanding domains of the computing sciences. The importance of the domain is in terms of the CPU and the memory requirements that shall be used by the system to compute the res...
Multiple Vehicles Semi-Self-driving System Using GNSS Coordinate Tracking under Relative Position with Correction Algorithm
This paper describes a simple and low-cost semiself- driving system which is constructed without cameras or image processing. In addition, a position correction method is presented by using a vehicle dynamics. Convention...
Image segmentation by adaptive distance based on EM algorithm
This paper introduces a Bayesian image segmentation algorithm based on finite mixtures. An EM algorithm is developed to estimate parameters of the Gaussian mixtures. The finite mixture is a flexible and powerful pr...
A Circular Polarization RFID Tag for Medical Uses
The aim of this paper is to present Radio Frequency Identification (RFID) Tag. The use of this kind of antennas in the medical field has a great importance in making people's life easier and improving the way to get medi...