[LBS15] Formal Verification of UML2 Timing Diagrams Based on Time Petri Nets

Conférence Internationale avec comité de lecture : The 5th International Conference on Information Systems and Technologies (ICIST 2015), March 2015, pp.12-22, Istanbul, Turkey,

Auteurs: A. Louati , K. Barkaoui , Z. Sbai

Mots clés: UML, TD, TPN, TCTL, Real-Time, OCL.

Résumé: Unified Modeling Language (UML) uses the design notation in industry and academia projects. Interesting by the critical Real-Time System verification, it is important to ensure its dependability in order to avoid eventual errors. In this paper, we aim to extend the UML diagrams by adding a formal verification stage. We tackle with the UML2 timing diagram (TD), as interaction diagram for describing the system's behavior in temporal way. So, we give a formal description for TD using Time Petri Nets (TPN). Then, we propose a formal verification by means of Romeo Model Checker. In particular, we show how to formulate quantitative properties using TCTL (timed computation tree logic). In addition, we show how we can derive the TCTL formulae from Object Constraint Language-Real Time (OCL-RT) constraints. Finally, we illustrate the proposed approach through a real case study.

Commentaires: http://www.ijist.net/ICIST15/proceedings/START.htm (extended paper accepted in International Journal of Information Systems in the Service Sector, to appear in 2016)

BibTeX

@inproceedings {
	LBS15,
	title	=	"{Formal Verification of UML2 Timing Diagrams Based on Time Petri Nets}",
	author	=	" A. Louati and K. Barkaoui and Z. Sbai ",
	booktitle	=	"{The 5th International Conference on Information Systems and Technologies (ICIST 2015)}",
	year	=	2015,
	month	=	"March",
	pages	=	"12-22",
	address	=	"Istanbul, Turkey",
	note	=	"{http://www.ijist.net/ICIST15/proceedings/START.htm (extended paper accepted in International Journal of Information Systems in the Service Sector, to appear in 2016)}",
}