Automatic Generation Of Promela Code From Sequence Diagram With Imbricate Combined Fragments
Résumé: 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.
Mots-clès:
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
