Abdelkrim Amirat, Ahcen Menasria, Mouna Ait Oubelli and Nadia Younsi (2012) Automatic Generation of PROMELA Code from Sequence Diagram with Imbricate Combined Fragments. Second International Conference on Innovative Computing Technology (INTECH 2012) , Casablanca, Morocco
Scientific Publications
Important: This page is frozen. New documents are now available in the digital repository DSpace
Abstract
Formal verification of UML diagram
is the act of proving or disproving the correctness
of intended algorithms underlying a system with
respect to a certain formal specification or
property, using formal methods of mathematics.
The most widely used techniques for system or
software verification: Simulation and testing,
deductive verification and Model checking. Model
checking is a formal verification technique, in
which an abstract model of a system is testing
automatically to verify whether this model meets a
given specification. SPIN Model checker is a
popular open-source software tool, used by
thousands of people worldwide that can be used for
the formal verification of distributed software
systems, SPIN is understand PROMELA code and
properties are express in Linear Temporal
Logic(LTL). This article aims propose a method
for converting UML sequence diagrams with
imbricate combined fragment automatically to
PROMELA code to simulate the execution and to
verify properties written in Linear Temporal Logic
(LTL) with SPIN Model checker.
is the act of proving or disproving the correctness
of intended algorithms underlying a system with
respect to a certain formal specification or
property, using formal methods of mathematics.
The most widely used techniques for system or
software verification: Simulation and testing,
deductive verification and Model checking. Model
checking is a formal verification technique, in
which an abstract model of a system is testing
automatically to verify whether this model meets a
given specification. SPIN Model checker is a
popular open-source software tool, used by
thousands of people worldwide that can be used for
the formal verification of distributed software
systems, SPIN is understand PROMELA code and
properties are express in Linear Temporal
Logic(LTL). This article aims propose a method
for converting UML sequence diagrams with
imbricate combined fragment automatically to
PROMELA code to simulate the execution and to
verify properties written in Linear Temporal Logic
(LTL) with SPIN Model checker.
Information
| Item Type | Conference |
|---|---|
| Divisions |
» Laboratory of Computer Science and Mathematics |
| ePrint ID | 258 |
| Date Deposited | 2014-12-29 |
| Further Information | Google Scholar |
| URI | https://univ-soukahras.dz/en/publication/article/258 |
BibTex
@inproceedings{uniusa258,
title={Automatic Generation of PROMELA Code from Sequence Diagram with Imbricate Combined Fragments},
author={Abdelkrim Amirat, Ahcen Menasria, Mouna Ait Oubelli and Nadia Younsi},
year={2012},
booktitle={Second International Conference on Innovative Computing Technology (INTECH 2012)}
}
title={Automatic Generation of PROMELA Code from Sequence Diagram with Imbricate Combined Fragments},
author={Abdelkrim Amirat, Ahcen Menasria, Mouna Ait Oubelli and Nadia Younsi},
year={2012},
booktitle={Second International Conference on Innovative Computing Technology (INTECH 2012)}
}