[en] Offline trace checking is a procedure for evaluating requirements over
a log of events produced by a system. The goal of this paper 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 are: the TemPsy
language, a domain-specific specification language based on common
property specification patterns, and extended with new constructs; a
model-driven offline trace checking procedure based on the mapping of
requirements written in TemPsy into OCL (Object Constraint Language)
constraints on a conceptual model on execution traces, which can be
evaluated using an OCL checker; the implementation of this trace
checking procedure in the TemPsy-Check tool; the evaluation of the
scalability of TemPsy-Check and its comparison to a state-of-the-art
alternative technology. The proposed approach has been applied to a
case study developed in collaboration with a public service
organization, active in the domain of business process modeling for
eGovernment.
Research center :
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
Disciplines :
Computer science
Author, co-author :
Dou, Wei ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Bianculli, Domenico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Briand, Lionel ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Language :
English
Title :
A Model-Driven Approach to Offline Trace Checking of Temporal Properties with OCL