Reference : A Model-Driven Approach to Offline Trace Checking of Temporal Properties

	Document type :	Dissertations and theses : Doctoral thesis
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Computational Sciences
	To cite this reference:	http://hdl.handle.net/10993/29184

Title :	A Model-Driven Approach to Offline Trace Checking of Temporal Properties
Language :	English
Author, co-author :	Dou, Wei [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Publication date :	24-Oct-2016
Institution :	University of Luxembourg, ​Luxembourg, ​​Luxembourg
Name of the degree :	Docteur en Informatique
Supervisor :	Briand, Lionel
	Bianculli, Domenico
President of the jury :	State, Radu
Member of the jury :	Sabetzadeh, Mehrdad
	Pautasso, Cesare
	Furia, Carlo Alberto
Keywords :	[en] trace checking ; temporal properties ; property specification patterns ; model-driven engineering ; OCL
Abstract :	[en] Offline trace checking is a procedure for evaluating requirements over a log of events produced by a system. The goal of this thesis is to present a practical and scalable solution for the offline checking of the temporal requirements of a system, which can be used in contexts where model-driven engineering is already a practice, where temporal specifications should be written in a domain-specific language not requiring a strong mathematical background, and where relying on standards and industry-strength tools for property checking is a fundamental prerequisite. The main contributions of this thesis are: i) the TemPsy (Temporal Properties made easy) language, a pattern-based domain-specific language for the specification of temporal properties; ii) a model-driven trace checking procedure, which relies on an optimized mapping of temporal requirements written in TemPsy into Object Constraint Language (OCL) constraints on a conceptual model of execution traces; iii) a model-driven approach to violation information collection, which relies on the evaluation of OCL queries on an instance of the trace model; iv) three publicly-available tools: 1) TemPsy-Check and 2) TemPsy-Report, implementing, respectively, the trace checking and violation information collection procedures; 3) an interactive visualization tool for navigating and analyzing the violation information collected by TemPsy-Report; v) an evaluation of the scalability of TemPsy-Check and TemPsy-Report, when applied to the verification of real properties. The proposed approaches have been applied to and evaluated on a case study developed in collaboration with a public service organization, active in the domain of business process modeling for eGovernment. The experimental results show that TemPsy-Check is able to analyze traces with one million events in about two seconds, and TemPsy-Report can collect violation information from such large traces in less than ten seconds; both tools scale linearly with respect to the length of the trace.
Research centres :	Interdisciplinary Centre for Security, Reliability and Trust
Funders :	Fonds National de la Recherche - FnR
Target :	Researchers ; Professionals ; Students
Permalink :	http://hdl.handle.net/10993/29184

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Open access thesis-dou.pdf Author postprint 1.23 MB View/Open

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map