TY - GEN
T1 - A Model-Driven Approach to Trace Checking of Pattern-Based Temporal Properties
AU - Dou, Wei
AU - Bianculli, Domenico
AU - Briand, Lionel
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/11/7
Y1 - 2017/11/7
N2 - Trace checking is a procedure for evaluating requirements over a log of events produced by a system. This paper deals with the problem of performing trace checking of temporal properties expressed in TemPsy, a pattern-based specification language. The goal of the paper is to present a scalable and practical solution for trace checking, which can be used in contexts where relying on model-driven engineering standards and tools for property checking is a fundamental prerequisite.The main contributions of the paper are: a model-driven trace checking procedure, which relies on the efficient mapping of temporal requirements written in TemPsy into OCL constraints on a conceptual model of execution traces; the implementation of this trace checking procedure in the TEMPSY-CHECK tool; the evaluation of the scalability of TEMPSY-CHECK, applied to the verification of real properties derived from a case study of our industrial partner, including a comparison with a state-of-the-art alternative technology based on temporal logic. The results of the evaluation show the feasibility of applying our model-driven approach for trace checking in realistic settings: TEMPSY-CHECK scales linearly with respect to the length of the input trace and can analyze traces with one million events in about two seconds.
AB - Trace checking is a procedure for evaluating requirements over a log of events produced by a system. This paper deals with the problem of performing trace checking of temporal properties expressed in TemPsy, a pattern-based specification language. The goal of the paper is to present a scalable and practical solution for trace checking, which can be used in contexts where relying on model-driven engineering standards and tools for property checking is a fundamental prerequisite.The main contributions of the paper are: a model-driven trace checking procedure, which relies on the efficient mapping of temporal requirements written in TemPsy into OCL constraints on a conceptual model of execution traces; the implementation of this trace checking procedure in the TEMPSY-CHECK tool; the evaluation of the scalability of TEMPSY-CHECK, applied to the verification of real properties derived from a case study of our industrial partner, including a comparison with a state-of-the-art alternative technology based on temporal logic. The results of the evaluation show the feasibility of applying our model-driven approach for trace checking in realistic settings: TEMPSY-CHECK scales linearly with respect to the length of the input trace and can analyze traces with one million events in about two seconds.
KW - model-driven engineering
KW - OCL
KW - temporal properties
KW - Trace checking
UR - http://www.scopus.com/inward/record.url?scp=85040548444&partnerID=8YFLogxK
U2 - 10.1109/MODELS.2017.9
DO - 10.1109/MODELS.2017.9
M3 - Conference contribution
AN - SCOPUS:85040548444
T3 - Proceedings - ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems, MODELS 2017
SP - 323
EP - 333
BT - Proceedings - ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems, MODELS 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 20th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017
Y2 - 17 September 2017 through 22 September 2017
ER -