A Model-Driven Approach to Offline Trace Checking of Temporal Properties with OCL

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.