Reference : A Model-Driven Approach to Offline Trace Checking of Temporal Properties
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Computational Sciences
A Model-Driven Approach to Offline Trace Checking of Temporal Properties
Dou, Wei mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
University of Luxembourg, ​Luxembourg, ​​Luxembourg
Docteur en Informatique
Briand, Lionel mailto
Bianculli, Domenico mailto
State, Radu mailto
Sabetzadeh, Mehrdad mailto
Pautasso, Cesare mailto
Furia, Carlo Alberto mailto
[en] trace checking ; temporal properties ; property specification patterns ; model-driven engineering ; OCL
[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.
Interdisciplinary Centre for Security, Reliability and Trust
Fonds National de la Recherche - FnR
Researchers ; Professionals ; Students

File(s) associated to this reference

Fulltext file(s):

Open access
thesis-dou.pdfAuthor postprint1.23 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.