A Model-Driven Approach to Trace Checking of Pattern-Based Temporal Properties

Wei Dou, Domenico Bianculli, Lionel Briand

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems, MODELS 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages323-333
Number of pages11
ISBN (Electronic)9781538634929
DOIs
Publication statusPublished - 7 Nov 2017
Externally publishedYes
Event20th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017 - Austin, United States
Duration: 17 Sep 201722 Sep 2017

Publication series

NameProceedings - ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems, MODELS 2017

Conference

Conference20th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017
Country/TerritoryUnited States
CityAustin
Period17/09/1722/09/17

Keywords

  • model-driven engineering
  • OCL
  • temporal properties
  • Trace checking

Fingerprint

Dive into the research topics of 'A Model-Driven Approach to Trace Checking of Pattern-Based Temporal Properties'. Together they form a unique fingerprint.

Cite this