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.

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://www.univ-soukahras.dz/en/publication/article/258

BibTex