Reference : A Model-Driven Approach to Offline Trace Checking of Temporal Properties |
Dissertations and theses : Doctoral thesis | |||
Engineering, computing & technology : Computer science | |||
Computational Sciences | |||
http://hdl.handle.net/10993/29184 | |||
A Model-Driven Approach to Offline Trace Checking of Temporal Properties | |
English | |
Dou, Wei ![]() | |
24-Oct-2016 | |
University of Luxembourg, Luxembourg, Luxembourg | |
Docteur en Informatique | |
Briand, Lionel ![]() | |
Bianculli, Domenico ![]() | |
State, Radu ![]() | |
Sabetzadeh, Mehrdad ![]() | |
Pautasso, Cesare ![]() | |
Furia, Carlo Alberto ![]() | |
[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 | |
http://hdl.handle.net/10993/29184 |
File(s) associated to this reference | ||||||||||||||
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.