Doctoral thesis (Dissertations and theses)
A Model-Driven Approach to Offline Trace Checking of Temporal Properties
Dou, Wei
2016
 

Files


Full Text
thesis-dou.pdf
Author postprint (1.26 MB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
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 center :
Interdisciplinary Centre for Security, Reliability and Trust
Disciplines :
Computer science
Author, co-author :
Dou, Wei ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Language :
English
Title :
A Model-Driven Approach to Offline Trace Checking of Temporal Properties
Defense date :
24 October 2016
Institution :
Unilu - University of Luxembourg, Luxembourg, Luxembourg
Degree :
Docteur en Informatique
President :
Jury member :
Sabetzadeh, Mehrdad 
Pautasso, Cesare
Furia, Carlo Alberto
Focus Area :
Computational Sciences
Funders :
FNR - Fonds National de la Recherche [LU]
Available on ORBilu :
since 27 December 2016

Statistics


Number of views
248 (66 by Unilu)
Number of downloads
188 (44 by Unilu)

Bibliography


Similar publications



Contact ORBilu